ISO

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 .

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.

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 is contractible, or a singleton, if there is , called the center of contraction, such that for all :

The fiber of a map over a point is:

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 , so that for all the fiber is contractible.

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

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.

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.

ISO