From: coquand Date: Sat, 19 Dec 2015 18:25:41 +0000 (+0100) Subject: testEquiv X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=59a8fd242d0c5d78caba2fb47b37d0d8b6f43d3a;p=cubicaltt.git testEquiv --- diff --git a/examples/testEquiv.ctt b/examples/testEquiv.ctt index 496f6f8..a0155d0 100644 --- a/examples/testEquiv.ctt +++ b/examples/testEquiv.ctt @@ -105,4 +105,64 @@ idToId (A B : U) (w : equiv A B) = 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) + +