`isoToEquiv` 和 `iso` 的定义是什么？

Question

这是来自 2019 Cubical Agda intro paper.

它们不在 Cubical.Core.Everything 中，甚至 Cubical v0.1 库的文件内容搜索也没有为我找到任何结果。

{-# OPTIONS --cubical #-}

open import Cubical.Core.Everything
open import Data.Nat

data Pos : Set where
  pos1 : Pos
  x0 : Pos → Pos
  x1 : Pos → Pos

data Bin : Set where
  bin0 : Bin
  binPos : Pos → Bin

ℕ≃Bin : ℕ ≃ Bin
ℕ≃Bin = isoToEquiv (iso ℕ→Bin Bin→ℕ Bin→ℕ→Bin ℕ→Bin→ℕ)

我正在尝试将这个短片段放在运行开始附近。

Answer 1

您可以在 Cubical.Foundations.Isomorphism 和 Cubical.Foundations.Equiv

中找到它们

`isoToEquiv` 和 `iso` 的定义是什么？

What are the definitions for `isoToEquiv` and `iso`?

agda

cubical-type-theory