Isomorphism

Comparing two Zeros

Article

Background

I've just got a cubical type checker from Mortberg et all, and the first thing I wanted to try was connecting two different values of two different types. As you may know, the core thing of Type Theory is equality or isomorphism or equivalence (which is the same thing but in different universes: 0, 1, 2, ...). Although cubical is U : U, this task is possible here.

So I will try a simple comparison of two nat types.

$ cat isoPath.ctt data nat = zero | suc (n : nat) data nat2 = zero2 | suc2 (n : nat2) $ cubical isoPath.ctt > nat EVAL: nat > nat2 EVAL: nat2

In MLTT, propositional equality in some sense reflects definitional which is usually built into typechecker. Everything that involves comparison of normalized terms stems from definitional equality.

The groupoid model gives us ∞-dimentional equality and also denies the uniqueness of identity proofs. That means we can build paths between objects in many distinguishable ways and the space of terms is ∞-groupoid:

Path (A : U) : U = (a b : A) -> PathP (<i> A) a b prop (A : U) : U = (a b : A) -> Path A a b set (A : U) : U = (a b : A) -> prop (Path A a b) groupoid (A : U) : U = (a b : A) -> set (Path A a b) gr_2 (A : U) : U = (a b : A) -> groupoid (Path A a b) gr_3 (A : U) : U = (a b : A) -> gr_2 (Path A a b)

n-Groupoid

mutual rec (A: U) (a b: A): (k: nat) -> U = split zero -> Path A a b succ n -> n_grpd (Path A a b) n n_grpd (A: U) (n: nat): U = (a b: A) -> ((rec A a b) n) prop (A: U): U = n_grpd A zero set (A: U): U = n_grpd A (succ zero) groupoid (A: U): U = n_grpd A (succ (succ zero))

∞-Groupoid

inf_grpd (A: U): U = (carrier: A) * (eq: (a b: A) -> Path A a b) * (next: (a b: A) -> inf_grpd (Path A a b)) * Unit

To model other types of equalities, we need to design their properties. The desired property, in general, is to compare incomparable things (heterogenous equality): namely two different points of two different types. The cubical built-in PathP type is exactly such equality. It connects different points of space with the function defined on interval $I=[0,1]$ that is smooth between values at interval edges.

Path between Elements

So let us be clear, we want to compare two points of A and B types which both live on U. At the higher level, we will use Path U A B which is homogenous on U. At the lower level we will use heterogenous PathP (Path U A B) a b:

PathTypes (A B: U) : U = PathP (<i> U) A B PathElem (A B: U) (a: A) (b: B) (P: PathTypes A B) : U = PathP P a b

Let's try to build a proof-term:

PathElem nat2 nat zero2 zero nat2nat

You may think of it as building proof of $0_A = 0_B$.

Path Isomorphism

But how to construct elements of Path U nat2 nat ?

nat2nat : Path U nat2 nat = isoPath nat2 nat toNat fromNat fromNatK toNatK

There is already an isoPath inside cubical. The proof-term of isoPath is implemented using glueing of types and composition primitives of type checker inside isoToEquiv lemma.

$$Iso(A,B) = \sum_{f:A\rightarrow B}\sum_{g:B\rightarrow A}\Biggl(\prod_{x:A} Id_A(gfx,x)) \times \prod_{y:B} Id_B(fgy,y)\Biggr)$$
isoPath (A B : U) (f : A -> B) (g : B -> A) (s : (y : B) -> Path B (f (g y)) y) (t : (x : A) -> Path A (g (f x)) x) : Path U A B = <i> Glue B [ (i = 0) -> (A,f,isoToEquiv A B f g s t), (i = 1) -> (B,idfun B,idIsEquiv B) ]

Contractability and Fibers

A type $A$ is contractible, or a singleton, if there is $a : A$, called the center of contraction, such that $a = x$ for all $x : A$:

$$isContr(A) = \sum_{a:A}\prod_{x:A} a = x$$.

The fiber of a map $f : A \rightarrow B$ over a point $y : B$ is:

$$fib_f(y) = \sum f x = y$$.
isContr (A : U) : U = (x : A) * ((y : A) -> Path A x y) fiber (A B : U) (f : A -> B) (y : B) : U = (x : A) * Path B y (f x) refl (A : U) (a : A) : Path A a a = <i> a contrSingl (A : U) (a b : A) (p : Path A a b) : Path (singl A a) (a,refl A a) (b,p) = <i> (p @ i,<j> p @ i/\j)

Equivalence

isEquiv is a contractible map $f: A \rightarrow B$, so that for all $y:B$ the fiber $fib_f(y)$ is contractible.

isEquiv (A B : U) (f : A -> B) : U = (y : B) -> isContr (fiber A B f y)

$$Iso(A,B) \rightarrow Equiv(A,B)$$.
isoToEquiv (A B : U) (f : A -> B) (g : B -> A) (s : (y : B) -> Path B (f (g y)) y) (t : (x : A) -> Path A (g (f x)) x) : isEquiv A B f = \(y:B) -> ((g y,<i>s [email protected]),\ (z:fiber A B f y) -> lemIso A B f g s t y (g y) z.1 (<i>s [email protected]) z.2)
idIsEquiv (A : U) : isEquiv A A (idfun A) = \(a : A) -> ((a, refl A a),\(z : fiber A A (idfun A) a) -> contrSingl A a z.1 z.2)

Commutative Square

For proving lemIso we need a simple commutative square term which is higher 2-path.

$\require{AMScd}$ \begin{CD} a_0 @>u>> a_1\\ @V r_0 V V= @VV r_1 V\\ b_0 @>>v> b_1 \end{CD}
Square (A : U) (a0 a1 b0 b1 : A) (u : Path A a0 a1) (v : Path A b0 b1) (r0 : Path A a0 b0) (r1 : Path A a1 b1) : U = PathP (<i> (PathP (<j> A) (u @ i) (v @ i))) r0 r1

Iso Lemma

lemIso (A B : U) (f : A -> B) (g : B -> A) (s : (y : B) -> Path B (f (g y)) y) (t : (x : A) -> Path A (g (f x)) x) (y : B) (x0 x1 : A) (p0 : Path B y (f x0)) (p1 : Path B y (f x1)) : Path (fiber A B f y) (x0,p0) (x1,p1) = <i> (p @ i,sq1 @ i) where rem0 : Path A (g y) x0 = <i> comp (<k> A) (g (p0 @ i)) [ (i = 1) -> t x0, (i = 0) -> <k> g y ] rem1 : Path A (g y) x1 = <i> comp (<k> A) (g (p1 @ i)) [ (i = 1) -> t x1, (i = 0) -> <k> g y ] p : Path A x0 x1 = <i> comp (<k> A) (g y) [ (i = 0) -> rem0, (i = 1) -> rem1 ] fill0 : Square A (g y) (g (f x0)) (g y) x0 (<i> g (p0 @ i)) rem0 (<i> g y) (t x0) = <i j> comp (<k> A) (g (p0 @ i)) [ (i = 1) -> <k> t x0 @ j /\ k, (i = 0) -> <k> g y, (j = 0) -> <k> g (p0 @ i) ] fill1 : Square A (g y) (g (f x1)) (g y) x1 (<i> g (p1 @ i)) rem1 (<i> g y) (t x1) = <i j> comp (<k> A) (g (p1 @ i)) [ (i = 1) -> <k> t x1 @ j /\ k, (i = 0) -> <k> g y, (j = 0) -> <k> g (p1 @ i) ] fill2 : Square A (g y) (g y) x0 x1 (<k> g y) p rem0 rem1 = <i j> comp (<k> A) (g y) [ (i = 0) -> <k> rem0 @ j /\ k, (i = 1) -> <k> rem1 @ j /\ k, (j = 0) -> <k> g y ] sq : Square A (g y) (g y) (g (f x0)) (g (f x1)) (<i> g y) (<i> g (f (p @ i))) (<j> g (p0 @ j)) (<j> g (p1 @ j)) = <i j> comp (<k> A) (fill2 @ i @ j) [ (i = 0) -> <k> fill0 @ j @ -k, (i = 1) -> <k> fill1 @ j @ -k, (j = 0) -> <k> g y, (j = 1) -> <k> t (p @ i) @ -k ] sq1 : Square B y y (f x0) (f x1) (<k>y) (<i> f (p @ i)) p0 p1 = <i j> comp (<k> B) (f (sq @ i @j)) [ (i = 0) -> s (p0 @ j), (i = 1) -> s (p1 @ j), (j = 1) -> s (f (p @ i)), (j = 0) -> s y ]

Now we need to pass maps $f$ and $g$:

toNat : nat2 -> nat = split zero2 -> zero suc2 n -> suc (toNat n) fromNat : nat -> nat2 = split zero -> zero2 suc n -> suc2 (fromNat n) toNatK : (n : nat2) -> Path nat2 (fromNat (toNat n)) n = split zero2 -> <_> zero2 suc2 n -> <i> suc2 (toNatK n @ i) fromNatK : (n : nat) -> Path nat (toNat (fromNat n)) n = split zero -> <_> zero suc n -> <i> suc (fromNatK n @ i)

Final Proof Term

Now let's see what we have built:

> PathElem nat2 nat zero2 zero nat2nat
EVAL: PathP ( Glue nat [ (!0 = 0) -> (nat2,(toNat,(\(y : B)
-> ((g y,<i> (s y) @ -i),\(z : fiber A B f y) -> lemIso A B f g
s t y (g y) z.1 (<i> (s y) @ -i) z.2)) (A = nat2, B = nat, f =
toNat, g = fromNat, s = fromNatK, t = toNatK))), (!0 = 1) ->
(nat,((\(a : A) -> a) (A = nat),(\(a : A) -> ((a,refl A a),\(z:
fiber A A (idfun A) a) -> contrSingl A a z.1 z.2)) (A = nat)))])
zero2 zero

And its normalized version:

> :n PathElem nat2 nat zero2 zero nat2nat
NORMEVAL: PathP ( Glue nat [ (!0 = 0) -> (nat2,(toNat,\(y
: nat) -> ((fromNat y, fromNatK y @ -!0),\(z : Sigma nat2
(\(x : nat2) -> PathP ( nat) y (toNat x))) ->  (comp
( nat2) (fromNat y) [ (!0 = 0) ->  comp ( nat2)
(fromNat (fromNatK y @ -!1)) [ (!1 = 0) ->  fromNat y,
(!1 = 1) ->  toNatK (fromNat y) @ !2 ], (!0 = 1) -> 
comp ( nat2) (fromNat (z.2 @ !1)) [ (!1 = 0) ->  fromNat y,
(!1 = 1) ->  toNatK z.1 @ !2 ] ], comp ( nat)
(toNat (comp ( nat2) (comp ( nat2) (fromNat y) [(!0 = 0)
->  comp ( nat2) (fromNat (fromNatK y @ (-!1 \/ -!2)))
[ (!1 = 0) ->  fromNat y, (!1 = 1)(!2 = 1) ->  toNatK
(fromNat y) @ !3, (!2 = 0) ->  fromNat y ], (!0 = 1) -> 
comp ( nat2) (fromNat (z.2 @ (!1 /\ !2))) [ (!1 = 0) -> 
fromNat y, (!1 = 1)(!2 = 1) ->  toNatK z.1 @ !3, (!2 = 0) ->
 fromNat y ], (!1 = 0) ->  fromNat y ]) [ (!0 = 0) -> 
comp ( nat2) (fromNat (fromNatK y @ -!1)) [ (!1 = 0) -> 
fromNat y, (!1 = 1) ->  toNatK (fromNat y) @ (-!2 /\ !3),
(!2 = 1) ->  fromNat (fromNatK y @ -!1) ], (!0 = 1) -> 
comp ( nat2) (fromNat (z.2 @ !1)) [ (!1 = 0) ->  fromNat
y, (!1 = 1) ->  toNatK z.1 @ (-!2 /\ !3), (!2 = 1) -> 
fromNat (z.2 @ !1) ], (!1 = 0) ->  fromNat y, (!1 = 1) ->
 toNatK (comp ( nat2) (fromNat y) [ (!0 = 0) -> 
comp ( nat2) (fromNat (fromNatK y @ -!1)) [ (!1 = 0) ->
 fromNat y, (!1 = 1) ->  toNatK (fromNat y) @ !2 ],
(!0 = 1) ->  comp ( nat2) (fromNat (z.2 @ !1)) [ (!1 = 0)
->  fromNat y, (!1 = 1) ->  toNatK z.1 @ !2 ] ]) @ -!2 ]))
[ (!0 = 0) ->  fromNatK (fromNatK y @ -!1) @ !2, (!0 = 1) ->
 fromNatK (z.2 @ !1) @ !2, (!1 = 0) ->  fromNatK y @ !2,
(!1 = 1) ->  fromNatK (toNat (comp ( nat2) (fromNat y)
[ (!0 = 0) ->  comp ( nat2) (fromNat (fromNatK y @ -!1))
[ (!1 = 0) ->  fromNat y, (!1 = 1) ->  toNatK (fromNat y)
@ !2 ], (!0 = 1) ->  comp ( nat2) (fromNat (z.2 @ !1))
[ (!1 = 0) ->  fromNat y, (!1 = 1) ->  toNatK z.1 @ !2 ] ]))
@ !2 ])))), (!0 = 1) -> (nat,(\(a : nat) -> a,\(a : nat) -> ((a, a),
\(z : Sigma nat (\(x : nat) -> PathP ( nat) a x)) -> 
(z.2 @ !0, z.2 @ (!0 /\ !1))))) ]) zero2 zero

The code is here.

Constructive Proofs of Heterogeneous Equalities in Cubical Type Theory