From: coquand <coquand@chalmers.se>
Date: Sat, 19 Dec 2015 18:25:41 +0000 (+0100)
Subject: testEquiv
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=59a8fd242d0c5d78caba2fb47b37d0d8b6f43d3a;p=cubicaltt.git

testEquiv
---

diff --git a/examples/testEquiv.ctt b/examples/testEquiv.ctt
index 496f6f8..a0155d0 100644
--- a/examples/testEquiv.ctt
+++ b/examples/testEquiv.ctt
@@ -105,4 +105,64 @@ idToId (A B : U) (w : equiv A B)
   = equivLemma A B (transEquiv A B (transEquivToId A B w)) w
       (<i>transIdFun A B w@-i)
 
+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)
+
+transEquivIsEquiv (A B : U)
+  : isEquiv (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)
+
+