From: coquand <coquand@chalmers.se>
Date: Fri, 18 Dec 2015 20:42:17 +0000 (+0100)
Subject: simpler version of idToId in testEquiv
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=f707d805f5c9c4fab79d950e239418621a465f94;p=cubicaltt.git

simpler version of idToId in testEquiv
---

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