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

0
votes

This is from the 2019 Cubical Agda intro paper.

They are not in Cubical.Core.Everything and even file content search for the Cubical v0.1 library is not turning up anything for me.

{-# 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→ℕ)

I am trying to get this short fragment near the start to run.

1
agdacubical-type-theory

1 Answers

2
votes

You can find those in Cubical.Foundations.Isomorphism and Cubical.Foundations.Equiv