simpler version of idToId in testEquiv

diff --git a/examples/testEquiv.ctt b/examples/testEquiv.ctt
new file mode 100644 (file)
index 0000000..70b188f
--- /dev/null
+++ b/examples/testEquiv.ctt
@@ -0,0 +1,111 @@
+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.1,invEq B B eB,retEq B B eB,secEq B B eB)\r
+             , (i = 0) -> (A,w.1,invEq A B w,retEq A B w,secEq A B 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.1,invEq A B e,retEq A B e,secEq A B e)\r
+           , (i = 1) -> (B,f.1,invEq B B f,retEq B B f,secEq B B f)\r
+           , (j = 1) -> (p@i,g.1,invEq Ai B g,retEq Ai B g,secEq Ai B g) ]\r
+\r
+transIdFun (A B : U) (w : equiv A B)\r
+  : Id (A -> B) (trans A B (transEquivToId A B w)) w.1 =\r
+  <i> \(a : A) -> let b : B = w.1 a\r
+                  in addf (f (f (f b))) b (addf (f (f b)) b (addf (f b) b (trf b))) @ i\r
+  where f (b : B) : B = comp (<_> B) b []\r
+        trf (b : B) : Id B (f b) b =\r
+          <i> fill (<_> B) b [] @ -i\r
+        addf (b b' : B) : Id B b b' -> Id B (f b) b' =\r
+          compId B (f b) b b' (trf 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
+      (transIdFun A B w)\r
+\r