From: coquand 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 = + (p0 a1@j, + \ (x:A) -> + comp (<_>A) (lem1 x@i@j) [ (i=0) -> p0 a1@j, (i=1) -> p0 x@(j\/k), + (j=0) -> p0 x@(i/\k), (j=1) -> 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 (Id A a0 (p1 x@i)) (p0 a1) (p0 x) = 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) -> \ (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 (P (p@i)) b0 b1 = + pP (p@i) (comp (P (p@i/\j)) b0 [(i=0) -> <_>b0]) (comp (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 = + (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 = + (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 = + ((w.2 (w.1 x)).2 (x,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 (p@-i) y [] + lem1 (x:A) : IdP p x (f x) = comp (p@(i/\j)) x [(i=0) -> x] + lem2 (y:B) : IdP p (g y) y = comp (p@(i\/-j)) y [(i=1) -> y] + lem3 (y:B) : Id B y (f (g y)) = comp p (g y) [(i=0) -> lem2 y,(i=1) -> lem1 (g y)] + lem4 (y:B) : IdP (Id (p@i) (lem2 y@i) (lem1 (g y)@i)) (g y) (lem3 y) = + 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 = + comp (p@-j) (q@i) [(i=0) -> lem2 y@-j,(i=1) -> lem1 x@-j] + lem6 (y:B) (x:A) (q:Id B y (f x)) : IdP (Id (p@i) (lem2 y@i) (lem1 x@i)) (lem5 y x q) q = + fill (p@-j) (q@i) [(i=0) -> lem2 y@-k,(i=1) -> lem1 x@-k] @ -j + lem7 (y:B) (x:A) (q:Id B y (f x)) : IdP (Id B y (f (lem5 y x q@i))) (lem3 y) q = + comp p (lem5 y x q@i/\j) [(i=0) -> lem2 y, (i=1) -> lem1 (lem5 y x q@j),(j=0) -> lem4 y@k@i,(j=1) -> 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 = + (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 (A) + +transEquivToId (A B : U) (w : equiv A B) : Id U A B = + 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 + = 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 ( 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 = + \(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 = + 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) +