other proof of univalence

diff --git a/examples/testEquiv.ctt b/examples/testEquiv.ctt
new file mode 100644 (file)
index 0000000..2b5dfee
--- /dev/null
+++ b/examples/testEquiv.ctt
@@ -0,0 +1,170 @@
+module testEquiv where\r
+\r
+import prelude\r
+\r
+fiber (A B : U) (f : A -> B) (y : B) : U =\r
+  (x : A) * Id B y (f x)\r
+\r
+isContr (A:U) : U = (a:A) * ((x:A) -> Id A a x)\r
+\r
+propIsContr (A:U) (z0 z1:isContr A) : Id (isContr A) z0 z1 =\r
+ <j>(p0 a1@j,\r
+     \ (x:A) -> \r
+        <i>comp (<_>A) (lem1 x@i@j) [ (i=0) -> <k>p0 a1@j, (i=1) -> <k>p0 x@(j\/k),\r
+                                      (j=0) -> <k>p0 x@(i/\k), (j=1) -> <k>p1 x@i ])\r
+ where\r
+  a0 : A = z0.1\r
+  p0 : (x:A) -> Id A a0 x = z0.2\r
+  a1 : A = z1.1\r
+  p1 : (x:A) -> Id A a1 x = z1.2\r
+  lem1 (x:A) : IdP (<i>Id A a0 (p1 x@i)) (p0 a1) (p0 x) = <i j> p0 (p1 x@i) @ j\r
+ \r
+isEquiv (A B : U) (f : A -> B) : U = (y:B) -> isContr (fiber A B f y)\r
+\r
+equiv (A B : U) : U = (f : A -> B) * isEquiv A B f\r
+\r
+propIsEquiv (A B : U) (f : A -> B)\r
+  : prop (isEquiv A B f) = \ (u0 u1:isEquiv A B f) -> <i> \ (y:B) -> propIsContr (fiber A B f y) (u0 y) (u1 y) @ i\r
+\r
+lemPropF (A : U) (P : A -> U) (pP : (x : A) -> prop (P x)) (a0 a1 :A) \r
+         (p : Id A a0 a1) (b0 : P a0) (b1 : P a1) : IdP (<i>P (p@i)) b0 b1 =\r
+ <i>pP (p@i) (comp (<j>P (p@i/\j)) b0 [(i=0) -> <_>b0]) (comp (<j>P (p@i\/-j)) b1 [(i=1) -> <_>b1])@i\r
+\r
+lemSig (A : U) (B : A -> U) (pB : (x : A) -> prop (B x))\r
+       (u v : (x:A) * B x) (p : Id A u.1 v.1) :\r
+       Id ((x:A) * B x) u v =\r
+  <i> (p@i,(lemPropF A B pB u.1 v.1 p u.2 v.2)@i)\r
+\r
+propSig (A : U) (B : A -> U) (pA : prop A)\r
+        (pB : (x : A) -> prop (B x)) (t u : (x:A) * B x) :\r
+        Id ((x:A) * B x) t u =\r
+  lemSig A B pB t u (pA t.1 u.1)\r
+\r
+equivLemma (A B : U)\r
+  : (v w : equiv A B) -> Id (A -> B) v.1 w.1 -> Id (equiv A B) v w\r
+  = lemSig (A -> B) (isEquiv A B) (propIsEquiv A B)\r
+\r
+-- for univalence\r
+\r
+invEq (A B:U) (w:equiv A B) (y:B) : A = (w.2 y).1.1\r
+\r
+retEq (A B:U) (w:equiv A B) (y:B) : Id B (w.1 (invEq A B w y)) y =\r
+ <i>(w.2 y).1.2@-i\r
+\r
+secEq (A B:U) (w:equiv A B) (x:A) : Id A (invEq A B w (w.1 x)) x =\r
+ <i> ((w.2 (w.1 x)).2 (x,<j>w.1 x)@i).1\r
+\r
+-- transDelta (A:U) : equiv A A = \r
+\r
+transEquiv (A B:U) (p:Id U A B) : equiv A B = (f,p)\r
+ where\r
+  f (x:A) : B = comp p x []\r
+  g (y:B) : A = comp (<i>p@-i) y []\r
+  lem1 (x:A) : IdP p x (f x) = <i>comp (<j>p@(i/\j)) x [(i=0) -> <j>x]\r
+  lem2 (y:B) : IdP p (g y) y = <i>comp (<j>p@(i\/-j)) y [(i=1) -> <j>y]\r
+  lem3 (y:B) : Id B y (f (g y)) = <i>comp p (g y) [(i=0) -> lem2 y,(i=1) -> lem1 (g y)]\r
+  lem4 (y:B) : IdP (<i>Id (p@i) (lem2 y@i) (lem1 (g y)@i)) (<j>g y) (lem3 y) =\r
+    <j i>fill p (g y) [(i=0) -> lem2 y,(i=1) -> lem1 (g y)] @ j\r
+  lem5 (y:B) (x:A) (q:Id B y (f x)) : Id A (g y) x = \r
+    <i>comp (<j>p@-j) (q@i) [(i=0) -> <j>lem2 y@-j,(i=1) -> <j>lem1 x@-j]\r
+  lem6 (y:B) (x:A) (q:Id B y (f x)) : IdP (<i>Id (p@i) (lem2 y@i) (lem1 x@i)) (lem5 y x q) q =\r
+    <j i>fill (<j>p@-j) (q@i) [(i=0) -> <k>lem2 y@-k,(i=1) -> <k>lem1 x@-k] @ -j\r
+  lem7 (y:B) (x:A) (q:Id B y (f x)) : IdP (<i>Id B y (f (lem5 y x q@i))) (lem3 y) q = \r
+    <j i>comp p (lem5 y x q@i/\j) [(i=0) -> lem2 y, (i=1) -> lem1 (lem5 y x q@j),(j=0) -> <k>lem4 y@k@i,(j=1) -> <k>lem6 y x q@k@i]\r
+  lem8 (y:B) : fiber A B f y = (g y,lem3 y)\r
+  lem9 (y:B) (z:fiber A B f y) : Id (fiber A B f y) (lem8 y) z =\r
+    <i>(lem5 y z.1 z.2@i,lem7 y z.1 z.2@i)\r
+  p (y:B) : isContr (fiber A B f y) = (lem8 y,lem9 y)\r
+\r
+transDelta (A:U) : equiv A A = transEquiv A A (<i>A)\r
+\r
+transEquivToId (A B : U) (w : equiv A B) : Id U A B =\r
+  <i> glue B [ (i = 1) -> (B,eB)\r
+             , (i = 0) -> (A,w) ]\r
+ where eB : equiv B B = transDelta B\r
+\r
+eqToEq (A B : U) (p : Id U A B)\r
+  : Id (Id U A B) (transEquivToId A B (transEquiv A B p)) p\r
+  = <j i> let e : equiv A B = transEquiv A B p\r
+              f : equiv B B = transDelta B\r
+              Ai : U = p@i\r
+              g : equiv Ai B = transEquiv Ai B (<k> p @ (i \/ k))\r
+          in glue B\r
+           [ (i = 0) -> (A,e)\r
+           , (i = 1) -> (B,f)\r
+           , (j = 1) -> (p@i,g)]\r
+\r
+test (A B : U) (w : equiv A B) : A -> B = trans A B (transEquivToId A B w)\r
+\r
+transIdFun (A B : U) (w : equiv A B)\r
+  : Id (A -> B) w.1 (trans A B (transEquivToId A B w)) =\r
+ <i> \ (a:A) -> \r
+   let b : B = w.1 a\r
+   in comp (<j> B) (comp (<j> B) (comp (<j> B) b [(i=0)-><j>b]) [(i=0)-><j>b]) [(i=0)-><j>b]\r
+\r
+idToId (A B : U) (w : equiv A B)\r
+  : Id (equiv A B) (transEquiv A B (transEquivToId A B w)) w\r
+  = 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