testEquiv

diff --git a/examples/testEquiv.ctt b/examples/testEquiv.ctt
index 496f6f869e471abb1e68a15ffc8ea5cfacf827c8..a0155d03a48be7750f3e93b87ea7574c2acc5c28 100644 (file)
--- 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\r
       (<i>transIdFun A B w@-i)\r
 \r
+lemIso (A B : U) (f : A -> B) (g : B -> A)\r
+       (s : (y : B) -> Id B (f (g y)) y)\r
+       (t : (x : A) -> Id A (g (f x)) x)\r
+       (y : B) (x0 x1 : A) (p0 : Id B y (f x0)) (p1 : Id B y (f x1)) :\r
+       Id (fiber A B f y) (x0,p0) (x1,p1) = <i> (p @ i,sq1 @ i)\r
+  where\r
+    rem0 : Id A (g y) x0 =\r
+      <i> comp (<_> A) (g (p0 @ i)) [ (i = 1) -> t x0, (i = 0) -> <_> g y ]\r
+\r
+    rem1 : Id A (g y) x1 =\r
+      <i> comp (<_> A) (g (p1 @ i)) [ (i = 1) -> t x1, (i = 0) -> <_> g y ]\r
+\r
+    p : Id A x0 x1 =\r
+     <i> comp (<_> A) (g y) [ (i = 0) -> rem0\r
+                            , (i = 1) -> rem1 ]\r
+\r
+    fill0 : Square A (g y) (g (f x0)) (g y) x0\r
+                     (<i> g (p0 @ i)) rem0 (<i> g y) (t x0)  =\r
+      <i j> comp (<_> A) (g (p0 @ i)) [ (i = 1) -> <k> t x0 @ j /\ k\r
+                                      , (i = 0) -> <_> g y\r
+                                      , (j = 0) -> <_> g (p0 @ i) ]\r
+\r
+    fill1 : Square A (g y) (g (f x1)) (g y) x1\r
+                     (<i> g (p1 @ i)) rem1 (<i> g y) (t x1) =\r
+      <i j> comp (<_> A) (g (p1 @ i)) [ (i = 1) -> <k> t x1 @ j /\ k\r
+                                      , (i = 0) -> <_> g y\r
+                                      , (j = 0) -> <_> g (p1 @ i) ]\r
+\r
+    fill2 : Square A (g y) (g y) x0 x1 \r
+                     (<_> g y) p rem0 rem1 =\r
+      <i j> comp (<_> A) (g y) [ (i = 0) -> <k> rem0 @ j /\ k\r
+                               , (i = 1) -> <k> rem1 @ j /\ k\r
+                               , (j = 0) -> <_> g y ]\r
+\r
+    sq : Square A (g y) (g y) (g (f x0)) (g (f x1)) \r
+                  (<i> g y) (<i> g (f (p @ i))) \r
+                  (<j> g (p0 @ j)) (<j> g (p1 @ j)) =\r
+      <i j> comp (<_> A) (fill2 @ i @ j) [ (i = 0) -> <k> fill0 @ j @ -k\r
+                                         , (i = 1) -> <k> fill1 @ j @ -k\r
+                                         , (j = 0) -> <_> g y\r
+                                         , (j = 1) -> <k> t (p @ i) @ -k ]\r
+\r
+    sq1 : Square B y y (f x0) (f x1) \r
+                   (<_>y) (<i> f (p @ i)) p0 p1 =\r
+      <i j> comp (<_> B) (f (sq @ i @j)) [ (i = 0) -> s (p0 @ j)\r
+                                         , (i = 1) -> s (p1 @ j)\r
+                                         , (j = 1) -> s (f (p @ i))\r
+                                         , (j = 0) -> s y ]\r
+\r
+gradLemma (A B : U) (f : A -> B) (g : B -> A)\r
+       (s : (y : B) -> Id B (f (g y)) y)\r
+       (t : (x : A) -> Id A (g (f x)) x) : isEquiv A B f = \r
+ \ (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)\r
+\r
+transEquivIsEquiv (A B : U)\r
+  : isEquiv (Id U A B) (equiv A B) (transEquiv A B)\r
+  = gradLemma (Id U A B) (equiv A B) (transEquiv A B)\r
+      (transEquivToId A B) (idToId A B) (eqToEq A B)\r
+\r
+\r
 \r