From: coquand Date: Sat, 26 Dec 2015 19:45:35 +0000 (+0100) Subject: other proof of univalence X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=f08b2e691293ddc2c6807711e88c91da4c14417b;p=cubicaltt.git other proof of univalence --- diff --git a/examples/testEquiv.ctt b/examples/testEquiv.ctt new file mode 100644 index 0000000..2b5dfee --- /dev/null +++ b/examples/testEquiv.ctt @@ -0,0 +1,170 @@ +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) + , (i = 0) -> (A,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) + , (i = 1) -> (B,f) + , (j = 1) -> (p@i,g)] + +test (A B : U) (w : equiv A B) : A -> B = trans A B (transEquivToId A B w) + +transIdFun (A B : U) (w : equiv A B) + : Id (A -> B) w.1 (trans A B (transEquivToId A B w)) = + \ (a:A) -> + let b : B = w.1 a + in comp ( B) (comp ( B) (comp ( B) b [(i=0)->b]) [(i=0)->b]) [(i=0)->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@-i) + +lemIso (A B : U) (f : A -> B) (g : B -> A) + (s : (y : B) -> Id B (f (g y)) y) + (t : (x : A) -> Id A (g (f x)) x) + (y : B) (x0 x1 : A) (p0 : Id B y (f x0)) (p1 : Id B y (f x1)) : + Id (fiber A B f y) (x0,p0) (x1,p1) = (p @ i,sq1 @ i) + where + rem0 : Id A (g y) x0 = + comp (<_> A) (g (p0 @ i)) [ (i = 1) -> t x0, (i = 0) -> <_> g y ] + + rem1 : Id A (g y) x1 = + comp (<_> A) (g (p1 @ i)) [ (i = 1) -> t x1, (i = 0) -> <_> g y ] + + p : Id A x0 x1 = + comp (<_> A) (g y) [ (i = 0) -> rem0 + , (i = 1) -> rem1 ] + + fill0 : Square A (g y) (g (f x0)) (g y) x0 + ( g (p0 @ i)) rem0 ( g y) (t x0) = + comp (<_> A) (g (p0 @ i)) [ (i = 1) -> t x0 @ j /\ k + , (i = 0) -> <_> g y + , (j = 0) -> <_> g (p0 @ i) ] + + fill1 : Square A (g y) (g (f x1)) (g y) x1 + ( g (p1 @ i)) rem1 ( g y) (t x1) = + comp (<_> A) (g (p1 @ i)) [ (i = 1) -> t x1 @ j /\ k + , (i = 0) -> <_> g y + , (j = 0) -> <_> g (p1 @ i) ] + + fill2 : Square A (g y) (g y) x0 x1 + (<_> g y) p rem0 rem1 = + comp (<_> A) (g y) [ (i = 0) -> rem0 @ j /\ k + , (i = 1) -> rem1 @ j /\ k + , (j = 0) -> <_> g y ] + + sq : Square A (g y) (g y) (g (f x0)) (g (f x1)) + ( g y) ( g (f (p @ i))) + ( g (p0 @ j)) ( g (p1 @ j)) = + comp (<_> A) (fill2 @ i @ j) [ (i = 0) -> fill0 @ j @ -k + , (i = 1) -> fill1 @ j @ -k + , (j = 0) -> <_> g y + , (j = 1) -> t (p @ i) @ -k ] + + sq1 : Square B y y (f x0) (f x1) + (<_>y) ( f (p @ i)) p0 p1 = + comp (<_> B) (f (sq @ i @j)) [ (i = 0) -> s (p0 @ j) + , (i = 1) -> s (p1 @ j) + , (j = 1) -> s (f (p @ i)) + , (j = 0) -> s y ] + +gradLemma (A B : U) (f : A -> B) (g : B -> A) + (s : (y : B) -> Id B (f (g y)) y) + (t : (x : A) -> Id A (g (f x)) x) : isEquiv A B f = + \ (y:B) -> ((g y,s y@-i),\ (z:fiber A B f y) -> lemIso A B f g s t y (g y) z.1 (s y@-i) z.2) + +transEquivIsEquiv (A B : U) + : isEquiv (Id U A B) (equiv A B) (transEquiv A B) + = gradLemma (Id U A B) (equiv A B) (transEquiv A B) + (transEquivToId A B) (idToId A B) (eqToEq A B) + + +