Add the proof of univalence using glue with isos

diff --git a/examples/equiv.ctt b/examples/equiv.ctt
index 1e67a073cf678bcf14c98d0776c16388065dcb27..a17e562d4cc7e5581bf64285309871d125c0ff37 100644 (file)
--- a/examples/equiv.ctt
+++ b/examples/equiv.ctt
@@ -118,12 +118,21 @@ transDelta (A : U) : equiv A A = transEquiv A A (<_> A)
 \r
 invEquiv (A B : U) (f : A -> B) (is : isEquiv A B f) (y : B) : A = (is.1 y).1\r
 \r
+invEq (A B : U) (f : equiv A B) : B -> A = invEquiv A B f.1 f.2\r
+\r
+\r
 retEquiv (A B : U) (f : A -> B) (is : isEquiv A B f) (y : B) :\r
   Id B (f (invEquiv A B f is y)) y = (is.1 y).2\r
 \r
+retEq (A B : U) (f:equiv A B) : (y:B) -> Id B (f.1 (invEq A B f y)) y =\r
+ retEquiv A B f.1 f.2\r
+\r
 secEquiv (A B : U) (f : A -> B) (is : isEquiv A B f) (x : A) :\r
   Id A (invEquiv A B f is (f x)) x = <i> (is.2 (f x) (x, <_> f x) @ i).1\r
 \r
+secEq (A B : U) (f: equiv A B) : (x:A) -> Id A (invEq A B f (f.1 x)) x =\r
+ secEquiv A B f.1 f.2\r
+\r
 \r
 \r
 \r

diff --git a/examples/univalence.ctt b/examples/univalence.ctt
index 1d4af7d2486829a3a3013a81b2af8f69feb751a2..cc77fbd37288a70e2bbef1c683532ae96e366e0b 100644 (file)
--- a/examples/univalence.ctt
+++ b/examples/univalence.ctt
@@ -3,25 +3,20 @@ module univalence where
 import gradLemma
 
 transEquivToId (A B : U) (w : equiv A B) : Id U A B =
-  <i> glue B [ (i=1) -> (B,transDelta B), (i=0) -> (A,w) ]
+  <i> glue B [ (i = 1) -> (B,eB.1,invEq B B eB,retEq B B eB,secEq B B eB)
+             , (i = 0) -> (A,w.1,invEq A B w,retEq A B w,secEq A B w) ]
+ where eB : equiv B B = transDelta B
 
 eqToEq (A B : U) (p : Id U A B)
   : Id (Id U A B) (transEquivToId A B (transEquiv A B p)) p
-  = <j i> glue B
-           [ (i=0) -> (A,transEquiv A B p)
-           , (i=1) -> (B,transDelta B)
-           , (j=1) -> (p@i,transEquiv (p@i) B (<k> p @ (i \/ k)))]
-
--- The normal form of this is much bigger than the normal form of eqToEq
-eqToEq' (A : U) : (B : U) (p : Id U A B)
-  -> Id (Id U A B) (transEquivToId A B (transEquiv A B p)) p
-  = J U A
-      (\ (B : U) (p : Id U A B) ->
-         Id (Id U A B) (transEquivToId A B (transEquiv A B p)) p)
-      (<j i> glue A
-           [ (i=0) -> (A,transDelta A)
-           , (i=1) -> (A,transDelta A)
-           , (j=1) -> (A,transDelta A)])
+  = <j i> let e : equiv A B = transEquiv A B p
+              f : equiv B B = transDelta B
+              Ai : U = p@i
+              g : equiv Ai B = transEquiv Ai B (<k> p @ (i \/ k))
+          in glue B
+           [ (i = 0) -> (A,e.1,invEq A B e,retEq A B e,secEq A B e)
+           , (i = 1) -> (B,f.1,invEq B B f,retEq B B f,secEq B B f)
+           , (j = 1) -> (p@i,g.1,invEq Ai B g,retEq Ai B g,secEq Ai B g) ]
 
 transIdFun (A B : U) (w : equiv A B)
   : Id (A -> B) (trans A B (transEquivToId A B w)) w.1 =
@@ -43,56 +38,8 @@ univalence (A B : U) : equiv (Id U A B) (equiv A B) =
   (transEquiv A B,gradLemma (Id U A B) (equiv A B) (transEquiv A B)
                             (transEquivToId A B) (idToId A B) (eqToEq A B))
 
-
--- Alternative definition:
-
--- Any equality defines an equivalence
-idToEquiv (A : U) : (B : U) -> Id U A B -> equiv A B =
-  J U A (\ (B : U) (_ : Id U A B) -> equiv A B) (idEquiv A)
-
-equivId (A B : U) (f : A -> B) (s : (y : B) -> fiber A B f y)
-        (t : (y : B) (w : fiber A B f y) -> Id (fiber A B f y) (s y) w)
-  : Id U A B = <i> glue B [ (i = 1) -> (B,idEquiv B), (i = 0) -> (A,f,s,t)]
-
-equivToId (A B : U) (w : equiv A B) : Id U A B =
-  <i> glue B [ (i = 1) -> (B,idEquiv B), (i = 0) -> (A,w) ]
-
-idToEquivIdFun (A B : U) (w : equiv A B)
-  : Id (A -> B) (idToEquiv A B (equivToId A B w)).1 w.1 =
-  <i> \(a : A) -> let b : B = w.1 (fill (<_> A) a [] @ -i)
-                  in (addf (f (f b)) b (addf (f b) b (trf b))) @ i
-  where p : A -> B = (idToEquiv A B (equivToId A B w)).1
-        f (b : B) : B = comp (<_> B) b []
-        trf (b : B) : Id B (f b) b =
-          <i> fill (<_> B) b [] @ -i
-        addf (b b' : B) : Id B b b' -> Id B (f b) b' =
-          compId B (f b) b b' (trf b)
-
-idToEquivK (A B : U) (w : equiv A B) : Id (equiv A B) (idToEquiv A B (equivToId A B w)) w =
-  lemSig (A -> B) (isEquiv A B) (propIsEquiv A B)
-    (idToEquiv A B (equivToId A B w)) w (idToEquivIdFun A B w)
-
 -- This takes too long to normalize:
-test (A : U) : Id (equiv A A) (idToEquiv A A (equivToId A A (idEquiv A))) (idEquiv A) =
-  idToEquivK A A (idEquiv A)
-
-
-
-
-
-
-
--- Old code:
--- -- we do something simpler than univalence
-
--- transpIsEquiv (A B:U) (p:Id U A B) : isEquiv A B (\ (x:A) -> transport p x) =
---  transport (<i>isEquiv A (p@i) (\ (x:A) -> transport (<j>p@i/\j) x)) (idIsEquiv A)
-
--- IdToEquiv (A B:U) (p: Id U A B) : Equiv A B = (\ (x:A) -> transport p x, transpIsEquiv A B p)
-
--- EquivToId (A B:U) (z:Equiv A B) : Id U A B = isEquivEq A B z.1 z.2
+test (A : U) : Id (equiv A A) (transEquiv A A (transEquivToId A A (idEquiv A))) (idEquiv A) =
+  idToId A A (idEquiv A)
 
--- secIdEquiv (A B :U) (p : Id U A B) : Id (Id U A B) (EquivToId A B (IdToEquiv A B p)) p =
---  transport (<i>Id (Id U A (p@i)) (EquivToId A (p@i) (IdToEquiv A (p@i) (<j>p@i/\j))) (<j>p@i/\j))
---            (<i>isoIdRef A@-i)