From: Anders Mörtberg <andersmortberg@gmail.com>
Date: Thu, 31 Dec 2015 08:03:46 +0000 (+0100)
Subject: Make aim.ctt compile
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=d4d4844b16bd521444bc445dec9cf9d10765deac;p=cubicaltt.git

Make aim.ctt compile
---

diff --git a/examples/aim.ctt b/examples/aim.ctt
index 4635e41..9608695 100644
--- a/examples/aim.ctt
+++ b/examples/aim.ctt
@@ -395,7 +395,7 @@ function from A to B:
 -- This gives a simple proof of subst (called transportf above and in
 -- UniMath):
 subst (A : U) (P : A -> U) (a b : A) (p : Id A a b) (e : P a) : P b =
-  transport (maponpaths A U P a b p) e
+  transport (cong A U P a b p) e
 
 
 -- Transport is defined in the Haskell code as a composition with an
@@ -474,19 +474,88 @@ We also want univalence and HITs.
                           Glueing
 --------------------------------------------------------------------------
 
-Glueing is a alternative form of univalence for producing non-trivial
-equalities from isomorphisms. In particular glueing gives a map from
-Iso(A,B) to A = B. This alternative form of univalence is useful for
-developing a lot of examples.
+Glueing is what enables us to prove univalence by producing
+non-trivial equalities from equivalences. In particular glueing gives
+a map from Equiv(A,B) to A = B.
 
 -}
 
+isContr (A : U) : U = (x : A) * ((y : A) -> Id A x y)
+
+fiber (A B : U) (f : A -> B) (y : B) : U =
+  (x : A) * Id B y (f x)
+
+isEquiv (A B : U) (f : A -> B) : U =
+  (y : B) -> isContr (fiber A B f y)
+
+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)
+
+-- Using the grad lemma we can transform isomorphisms into equalities.
+lemIso (A B : U) (f : A -> B) (g : B -> A)
+       (s : (y : B) -> Id B (f (g y)) y)
+       (t : (x : A) -> Id A (g (f x)) x)
+       (y : B) (x0 x1 : A) (p0 : Id B y (f x0)) (p1 : Id B y (f x1)) :
+       Id (fiber A B f y) (x0,p0) (x1,p1) = <i> (p @ i,sq1 @ i)
+  where
+    rem0 : Id A (g y) x0 =
+      <i> comp (<_> A) (g (p0 @ i)) [ (i = 1) -> t x0, (i = 0) -> <_> g y ]
+
+    rem1 : Id A (g y) x1 =
+      <i> comp (<_> A) (g (p1 @ i)) [ (i = 1) -> t x1, (i = 0) -> <_> g y ]
+
+    p : Id A x0 x1 =
+     <i> comp (<_> 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 (<_> A) (g (p0 @ i)) [ (i = 1) -> <k> t x0 @ j /\ k
+                                      , (i = 0) -> <_> g y
+                                      , (j = 0) -> <_> 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 (<_> A) (g (p1 @ i)) [ (i = 1) -> <k> t x1 @ j /\ k
+                                      , (i = 0) -> <_> g y
+                                      , (j = 0) -> <_> g (p1 @ i) ]
+
+    fill2 : Square A (g y) (g y) x0 x1 
+                     (<_> g y) p rem0 rem1 =
+      <i j> comp (<_> A) (g y) [ (i = 0) -> <k> rem0 @ j /\ k
+                               , (i = 1) -> <k> rem1 @ j /\ k
+                               , (j = 0) -> <_> 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 (<_> A) (fill2 @ i @ j) [ (i = 0) -> <k> fill0 @ j @ -k
+                                         , (i = 1) -> <k> fill1 @ j @ -k
+                                         , (j = 0) -> <_> g y
+                                         , (j = 1) -> <k> t (p @ i) @ -k ]
+
+    sq1 : Square B y y (f x0) (f x1) 
+                   (<_>y) (<i> f (p @ i)) p0 p1 =
+      <i j> comp (<_> 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 ]
+
+gradLemma (A B : U) (f : A -> B) (g : B -> A)
+       (s : (y : B) -> Id B (f (g y)) y)
+       (t : (x : A) -> Id A (g (f x)) x) : isEquiv A B f = 
+ \ (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)
+
+
 
 isoId (A B : U) (f : A -> B) (g : B -> A)
       (s : (y : B) -> Id B (f (g y)) y)
       (t : (x : A) -> Id A (g (f x)) x) : Id U A B =
-      <i> glue A [ (i = 0) -> (A,idfun A,idfun A,refl A,refl A)
-                 , (i = 1) -> (B,g,f,t,s) ]
+       <i> glue B [ (i = 0) -> (A,f,gradLemma A B f g s t)
+                  , (i = 1) -> (B,idfun B,idIsEquiv B) ]
+
+
 
 
 
@@ -586,9 +655,6 @@ testNOneZ : Z = transport (<i> sucIdZ @ - i) zeroZ
 
 
 
-
-
-
 {-
                   Higher-inductive types (HITs)
 --------------------------------------------------------------------------