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.
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$:
The fiber of a map $f : A \rightarrow B$ over a point $y : B$ 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 $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)
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.
![]() |
Constructive Proofs of Heterogeneous Equalities in Cubical Type Theory |