-module equiv where\r
-\r
-import prelude\r
-\r
-fiber (A B : U) (f : A -> B) (y : B) : U =\r
- (x : A) * Id B (f x) y\r
-\r
-isEquiv (A B : U) (f : A -> B) : U =\r
- (s : (y : B) -> fiber A B f y)\r
- * ((y : B) (w : fiber A B f y) -> Id (fiber A B f y) (s y) w)\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) = lemProp (isEquiv A B f) lem\r
- where\r
- isEqf : U = isEquiv A B f\r
- fibf : (y : B) -> U = fiber A B f\r
- center : U = (y : B) -> fibf y\r
- isCenter (s : center) : U = (y : B) (w : fibf y) -> Id (fibf y) (s y) w\r
- lem (fe : isEqf) : prop isEqf = propSig center isCenter pc pisc\r
- where\r
- fibprop (y : B) (u v : fibf y) : Id (fibf y) u v =\r
- compId (fibf y) u (fe.1 y) v (<i> fe.2 y u @ -i) (fe.2 y v)\r
- pc : prop center = propPi B fibf fibprop\r
- pisc (s : center) (g h : isCenter s) : Id (isCenter s) g h =\r
- <i> \ (y : B) (w : fibf y) ->\r
- propSet (fibf y) (fibprop y) (s y) w (g y w) (h y w) @ i\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
-\r
--- The identity function is an equivalence\r
-idCenter (A : U) (y : A) : fiber A A (idfun A) y = (y, refl A y)\r
-\r
--- TODO: redifine fiber so this gets nicer?\r
-idIsCenter (A : U) (y : A) (w : fiber A A (idfun A) y)\r
- : Id (fiber A A (idfun A) y) (idCenter A y) w =\r
- <i> (w.2 @ -i, <j> w.2 @ j \/ -i)\r
-\r
-idIsEquiv (A : U) : isEquiv A A (idfun A) = (idCenter A,idIsCenter A)\r
-\r
-idEquiv (A : U) : equiv A A = (idfun A, idIsEquiv A)\r
-\r
--- Transport is an equivalence\r
--- NB: The proof is taken from the output of a comp U\r
-trans (A B : U) (p : Id U A B) (a : A) : B = transport p a\r
-\r
-transCenter (A B : U) (p : Id U A B) (y : B) : fiber A B (trans A B p) y =\r
- (comp (<i0> p @ -i0) y []\r
- ,<i0> comp p (comp (<i0> p @ -i0) y [])\r
- [ (i0 = 0) -> <i1> comp (<i2> p @ (i1 /\ i2)) (comp (<i0> p @ -i0) y [])\r
- [ (i1 = 0) -> <i2> comp (<i0> p @ -i0) y [] ]\r
- , (i0 = 1) -> <i1> comp (<i2> p @ (i1 \/ -i2)) y [ (i1 = 1) -> <i2> y ] ])\r
-\r
-transIsCenter (A B : U) (p : Id U A B) (y : B) (w : fiber A B (trans A B p) y)\r
- : Id (fiber A B (trans A B p) y) (transCenter A B p y) w\r
- = <i0>\r
- ( comp (<i1> p @ -i1) (w.2 @ -i0)\r
- [ (i0 = 0) -> <i1> comp (<i2> p @ (-i1 \/ -i2)) y [ (i1 = 0) -> <i2> y ]\r
- , (i0 = 1) -> <i1> comp (<i2> p @ (-i1 /\ i2)) (w.1) [ (i1 = 1) -> <i2> w.1 ] ]\r
- , <i1> comp (<i2> p @ i2)\r
- (comp (<i2> p @ -i2) (w.2 @ (-i0 \/ i1))\r
- [ (i0 = 0) -> <i2> comp (<i3> p @ (-i2 \/ -i3)) y [ (i2 = 0) -> <i3> y ]\r
- , (i0 = 1)(i1 = 0) ->\r
- <i2> comp (<i3> p @ (-i2 /\ i3)) (w.1)\r
- [ (i2 = 1) -> <i3> w.1 ]\r
- , (i1 = 1) -> <i2> comp (<i3> p @ (-i2 \/ -i3)) y [ (i2 = 0) -> <i3> y ] ])\r
- [ (i0 = 0) -> <i2> comp (<i3> p @ (i2 /\ i3))\r
- (comp (<i0> p @ -i0) y [ ])\r
- [ (i1 = 0) ->\r
- <i3> comp (<i4> p @ (i2 /\ i3 /\ i4))\r
- (comp (<i0> p @ -i0) y [ ])\r
- [ (i2 = 0) -> <i4> comp (<i0> p @ -i0) y [ ]\r
- , (i3 = 0) -> <i4> comp (<i0> p @ -i0) y [ ] ]\r
- , (i1 = 1) ->\r
- <i3> comp (<i4> p @ ((i2 /\ i3) \/ -i4)) y\r
- [ (i2 = 1)(i3 = 1) -> <i4> y ]\r
- , (i2 = 0) -> <i3> comp (<i0> p @ -i0) y [ ] ]\r
- , (i0 = 1) ->\r
- <i2> comp (<i3> p @ (i2 \/ -i3)) (w.2 @ i1)\r
- [ (i1 = 0) ->\r
- <i3> comp (<i4> p @ ((i2 /\ i4) \/ (-i3 /\ i4))) (w.1)\r
- [ (i2 = 0)(i3 = 1) -> <i4> w.1 ]\r
- , (i1 = 1) ->\r
- <i3> comp (<i4> p @ (i2 \/ -i3 \/ -i4)) y\r
- [ (i2 = 1) -> <i4> y, (i3 = 0) -> <i4> y ]\r
- , (i2 = 1) -> <i3> w.2 @ i1 ]\r
- , (i1 = 0) ->\r
- <i2> comp (<i3> p @ (i2 /\ i3))\r
- (comp (<i1> p @ -i1) (w.2 @ -i0)\r
- [ (i0 = 0) ->\r
- <i1> comp (<i2> p @ (-i1 \/ -i2)) y [ (i1 = 0) -> <i2> y ]\r
- , (i0 = 1) ->\r
- <i1> comp (<i2> p @ (-i1 /\ i2)) (w.1)\r
- [ (i1 = 1) -> <i2> w.1 ]\r
- ])\r
- [ (i2 = 0) ->\r
- <i3> comp (<i1> p @ -i1) (w.2 @ -i0)\r
- [ (i0 = 0) ->\r
- <i1> comp (<i2> p @ (-i1 \/ -i2)) y\r
- [ (i1 = 0) -> <i2> y ]\r
- , (i0 = 1) ->\r
- <i1> comp (<i2> p @ (-i1 /\ i2)) (w.1)\r
- [ (i1 = 1) -> <i2> w.1 ]\r
- ]\r
- ]\r
- , (i1 = 1) -> <i2> comp (<i3> p @ (i2 \/ -i3)) y [ (i2 = 1) -> <i3> y ] ]\r
- )\r
-\r
-transIsEquiv (A B : U) (p : Id U A B) : isEquiv A B (trans A B p) =\r
- (transCenter A B p,transIsCenter A B p)\r
-\r
-transEquiv (A B : U) (p : Id U A B) : equiv A B =\r
- (trans A B p,transIsEquiv A B p)\r
-\r
-transDelta (A : U) : equiv A A = transEquiv A A (<_> A)\r
-\r
-\r
-invEquiv (A B : U) (f : A -> B) (is : isEquiv A B f) (y : B) : A = (is.1 y).1\r
-\r
-invEq (A B : U) (f : equiv A B) : B -> A = invEquiv A B f.1 f.2\r
-\r
-\r
-retEquiv (A B : U) (f : A -> B) (is : isEquiv A B f) (y : B) :\r
- Id B (f (invEquiv A B f is y)) y = (is.1 y).2\r
-\r
-retEq (A B : U) (f:equiv A B) : (y:B) -> Id B (f.1 (invEq A B f y)) y =\r
- retEquiv A B f.1 f.2\r
-\r
-secEquiv (A B : U) (f : A -> B) (is : isEquiv A B f) (x : A) :\r
- Id A (invEquiv A B f is (f x)) x = <i> (is.2 (f x) (x, <_> f x) @ i).1\r
-\r
-secEq (A B : U) (f: equiv A B) : (x:A) -> Id A (invEq A B f (f.1 x)) x =\r
- secEquiv A B f.1 f.2\r
-\r
-\r
--- Alternative definition:\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
-\r
-\r
-\r
--- Another alternative definitions:\r
-\r
--- isContr (A : U) : U = and (prop A) A\r
-\r
--- fiber (A B:U) (f:A->B) (b:B) : U = (x:A) * Id B b (f x)\r
-\r
--- lemIdFib (A:U) (a:A) : prop (fiber A A (\ (x:A) -> x) a) = rem\r
--- where F : U = fiber A A (\ (x:A) -> x) a\r
--- rem (u v:F) : Id F u v = <i>(rem1 @ i,rem2 @ i)\r
--- where x : A = u.1\r
--- p : Id A a x = u.2\r
--- y : A = v.1\r
--- q : Id A a y = v.2\r
--- rem1 : Id A x y = <i>comp A a [(i=0) -> p,(i=1) -> q]\r
--- rem2 : IdP (<i>Id A a (rem1@i)) p q = <i j>comp A a [(i=0) -> <l>p@(j/\l),(i=1) -> <l>q@(j/\l)]\r
-\r
--- lemPropAnd (A B :U) (pA: prop A) (pB: A -> prop B) : prop (and A B) = \r
--- \ (u v:and A B) -> <i>((pA u.1 v.1)@i, (pB u.1 u.2 v.2)@i)\r
-\r
--- isContrProp (A:U) : prop (isContr A) = \r
--- lemPropAnd (prop A) A (propIsProp A) (\ (h:prop A) -> h)\r
-\r
--- isEquiv (A B:U) (f:A->B) : U = (y:B) -> isContr (fiber A B f y)\r
-\r
--- idIsEquiv (A:U) : isEquiv A A (idfun A) = \ (a:A) -> (lemIdFib A a,(a,refl A a))\r
-\r
--- propIsEquiv (A B : U) (f : A -> B) : prop (isEquiv A B f)\r
--- = propPi B (\ (y:B) -> isContr (fiber A B f y)) (\ (y:B) -> isContrProp (fiber A B f y))\r
-\r
--- isEquivEq (A B : U) (f : A -> B) (is:isEquiv A B f) : Id U A B = \r
--- isoId A B f g (\ (y:B) -> <i>(s y)@-i) t\r
--- where\r
--- rem1 (y:B) : prop (fiber A B f y) = (is y).1\r
--- rem2 (y:B) : fiber A B f y = (is y).2\r
--- g (y:B) : A = (rem2 y).1\r
--- s (y:B) : Id B y (f (g y)) = (rem2 y).2\r
--- rem3 (x:A) : Id B (f x) (f (g (f x))) = s (f x)\r
--- rem4 (x:A) : Id (fiber A B f (f x)) (g (f x),rem3 x) (x,refl B (f x)) = \r
--- rem1 (f x) (g (f x),rem3 x) (x,refl B (f x))\r
--- t (x:A) : Id A (g (f x)) x = <i> ((rem4 x)@i).1\r
- \r
--- Equiv (A B : U) : U = (f : A -> B) * isEquiv A B f\r
-\r
--- lemIdEquiv (A B:U) (f g : Equiv A B) (h:Id (A->B) f.1 g.1) : Id (Equiv A B) f g\r
--- = <i>(h@i,(lemPropF (A->B) (isEquiv A B) (propIsEquiv A B) f.1 g.1 h f.2 g.2)@i)\r
-\r
--- -- a general lemma about equivalence and fibrations\r
-\r
--- Sigma (A:U) (F:A->U) : U = (x:A) * F x\r
-\r
--- lemEquivFib (A:U) (F G :A -> U) (f:(x:A) -> F x -> G x)\r
--- (h : isEquiv (Sigma A F) (Sigma A G) (\ (xp : Sigma A F) -> (xp.1,f xp.1 xp.2))) (x:A) (v:G x) : \r
--- isContr (fiber (F x) (G x) (f x) v) = (rem7,psi (rem1.2))\r
--- where\r
--- AF : U = Sigma A F\r
--- AG : U = Sigma A G\r
--- g (xp : AF) : AG = (xp.1,f xp.1 xp.2)\r
--- rem1 : isContr (fiber AF AG g (x,v)) = h (x,v)\r
--- phi (z:fiber (F x) (G x) (f x) v) : fiber AF AG g (x,v) = ((x,z.1),<i>(x,(z.2)@ i))\r
--- psi (z:fiber AF AG g (x,v)) : fiber (F x) (G x) (f x) v = transport (<i> (u : F (p@-i)) * IdP (<j>G (p@-i /\ j)) v (f (p@-i) u)) (w,q)\r
--- where yu : AF = z.1\r
--- y : A = yu.1\r
--- w : F y = yu.2\r
--- p : Id A x y = <i>(z.2 @ i).1\r
--- q : IdP (<j>G (p@j)) v (f y w) = <i>((z.2) @ i).2\r
--- rem7 (z0 z1 : fiber (F x) (G x) (f x) v) : Id (fiber (F x) (G x) (f x) v) z0 z1 = <i>psi ((rem1.1 (phi z0) (phi z1))@i)\r
-\r
+-- This file contains the definition of equivalences and various
+-- results on these, including the "graduate lemma".
+module equiv 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)
+
+lemSinglContr (A:U) (a:A) : isContr ((x:A) * Id A a x) =
+ ((a,refl A a),\ (z:(x:A) * Id A a x) -> contrSingl A a z.1 z.2)
+
+idEquiv (A:U) : equiv A A = (\ (x:A) -> x, lemSinglContr A)
+
+transEquiv (A X:U) (p:Id U A X) : equiv A X =
+ substTrans U (equiv A) A X p (idEquiv A)
+
+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)
+ , (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
+ = <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)
+ , (i = 1) -> (B,f)
+ , (j = 1) -> (p@i,g)]
+
+test (A B : U) (w : equiv A B) (x:A) : B = (transEquiv A B (transEquivToId A B w)).1 x
+
+transIdFun (A B : U) (w : equiv A B)
+ : Id (A -> B) w.1 (transEquiv A B (transEquivToId A B w)).1 =
+ <i> \ (a:A) ->
+ let b : B = w.1 a
+ u : A = comp (<j>A) a []
+ q : Id B (w.1 u) b = <i>w.1 (comp (<j>A) a [(i=1) -> <j>a])
+ in comp (<j> B)
+ (comp (<j> B) (comp (<j> B) (comp (<j> B) (w.1 u) [(i=0)->q]) [(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
+ (<i>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) = <i> (p @ i,sq1 @ i)
+ where
+ rem0 : Id A (g y) x0 =
+ <i> comp (<_> A) (g (p0 @ i)) [ (i = 1) -> t x0, (i = 0) -> <_> g y ]
+
+ rem1 : Id A (g y) x1 =
+ <i> comp (<_> A) (g (p1 @ i)) [ (i = 1) -> t x1, (i = 0) -> <_> g y ]
+
+ p : Id A x0 x1 =
+ <i> comp (<_> A) (g y) [ (i = 0) -> rem0
+ , (i = 1) -> rem1 ]
+
+ fill0 : Square A (g y) (g (f x0)) (g y) x0
+ (<i> g (p0 @ i)) rem0 (<i> g y) (t x0) =
+ <i j> comp (<_> A) (g (p0 @ i)) [ (i = 1) -> <k> t x0 @ j /\ k
+ , (i = 0) -> <_> g y
+ , (j = 0) -> <_> g (p0 @ i) ]
+
+ fill1 : Square A (g y) (g (f x1)) (g y) x1
+ (<i> g (p1 @ i)) rem1 (<i> g y) (t x1) =
+ <i j> comp (<_> A) (g (p1 @ i)) [ (i = 1) -> <k> 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 =
+ <i j> comp (<_> A) (g y) [ (i = 0) -> <k> rem0 @ j /\ k
+ , (i = 1) -> <k> rem1 @ j /\ k
+ , (j = 0) -> <_> g y ]
+
+ sq : Square A (g y) (g y) (g (f x0)) (g (f x1))
+ (<i> g y) (<i> g (f (p @ i)))
+ (<j> g (p0 @ j)) (<j> g (p1 @ j)) =
+ <i j> comp (<_> A) (fill2 @ i @ j) [ (i = 0) -> <k> fill0 @ j @ -k
+ , (i = 1) -> <k> fill1 @ j @ -k
+ , (j = 0) -> <_> g y
+ , (j = 1) -> <k> t (p @ i) @ -k ]
+
+ sq1 : Square B y y (f x0) (f x1)
+ (<_>y) (<i> f (p @ i)) p0 p1 =
+ <i j> 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,<i>s y@-i),\ (z:fiber A B f y) -> lemIso A B f g s t y (g y) z.1 (<i>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)
+++ /dev/null
-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)
-
-lemSinglContr (A:U) (a:A) : isContr ((x:A) * Id A a x) =
- ((a,refl A a),\ (z:(x:A) * Id A a x) -> contrSingl A a z.1 z.2)
-
-idEquiv (A:U) : equiv A A = (\ (x:A) -> x, lemSinglContr A)
-
-transEquiv (A X:U) (p:Id U A X) : equiv A X =
- substTrans U (equiv A) A X p (idEquiv A)
-
-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)
- , (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
- = <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)
- , (i = 1) -> (B,f)
- , (j = 1) -> (p@i,g)]
-
-test (A B : U) (w : equiv A B) (x:A) : B = (transEquiv A B (transEquivToId A B w)).1 x
-
-transIdFun (A B : U) (w : equiv A B)
- : Id (A -> B) w.1 (transEquiv A B (transEquivToId A B w)).1 =
- <i> \ (a:A) ->
- let b : B = w.1 a
- u : A = comp (<j>A) a []
- q : Id B (w.1 u) b = <i>w.1 (comp (<j>A) a [(i=1) -> <j>a])
- in comp (<j> B)
- (comp (<j> B) (comp (<j> B) (comp (<j> B) (w.1 u) [(i=0)->q]) [(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
- (<i>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) = <i> (p @ i,sq1 @ i)
- where
- rem0 : Id A (g y) x0 =
- <i> comp (<_> A) (g (p0 @ i)) [ (i = 1) -> t x0, (i = 0) -> <_> g y ]
-
- rem1 : Id A (g y) x1 =
- <i> comp (<_> A) (g (p1 @ i)) [ (i = 1) -> t x1, (i = 0) -> <_> g y ]
-
- p : Id A x0 x1 =
- <i> comp (<_> A) (g y) [ (i = 0) -> rem0
- , (i = 1) -> rem1 ]
-
- fill0 : Square A (g y) (g (f x0)) (g y) x0
- (<i> g (p0 @ i)) rem0 (<i> g y) (t x0) =
- <i j> comp (<_> A) (g (p0 @ i)) [ (i = 1) -> <k> t x0 @ j /\ k
- , (i = 0) -> <_> g y
- , (j = 0) -> <_> g (p0 @ i) ]
-
- fill1 : Square A (g y) (g (f x1)) (g y) x1
- (<i> g (p1 @ i)) rem1 (<i> g y) (t x1) =
- <i j> comp (<_> A) (g (p1 @ i)) [ (i = 1) -> <k> 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 =
- <i j> comp (<_> A) (g y) [ (i = 0) -> <k> rem0 @ j /\ k
- , (i = 1) -> <k> rem1 @ j /\ k
- , (j = 0) -> <_> g y ]
-
- sq : Square A (g y) (g y) (g (f x0)) (g (f x1))
- (<i> g y) (<i> g (f (p @ i)))
- (<j> g (p0 @ j)) (<j> g (p1 @ j)) =
- <i j> comp (<_> A) (fill2 @ i @ j) [ (i = 0) -> <k> fill0 @ j @ -k
- , (i = 1) -> <k> fill1 @ j @ -k
- , (j = 0) -> <_> g y
- , (j = 1) -> <k> t (p @ i) @ -k ]
-
- sq1 : Square B y y (f x0) (f x1)
- (<_>y) (<i> f (p @ i)) p0 p1 =
- <i j> 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,<i>s y@-i),\ (z:fiber A B f y) -> lemIso A B f g s t y (g y) z.1 (<i>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)
module testUniv where
import testContr
-import testEquiv
+import equiv
swap : bool -> bool = split
true -> false
--- /dev/null
+-- This file contains the old definition of equivalence and various\r
+-- results on these\r
+module equiv where\r
+\r
+import prelude\r
+\r
+fiber (A B : U) (f : A -> B) (y : B) : U =\r
+ (x : A) * Id B (f x) y\r
+\r
+isEquiv (A B : U) (f : A -> B) : U =\r
+ (s : (y : B) -> fiber A B f y)\r
+ * ((y : B) (w : fiber A B f y) -> Id (fiber A B f y) (s y) w)\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) = lemProp (isEquiv A B f) lem\r
+ where\r
+ isEqf : U = isEquiv A B f\r
+ fibf : (y : B) -> U = fiber A B f\r
+ center : U = (y : B) -> fibf y\r
+ isCenter (s : center) : U = (y : B) (w : fibf y) -> Id (fibf y) (s y) w\r
+ lem (fe : isEqf) : prop isEqf = propSig center isCenter pc pisc\r
+ where\r
+ fibprop (y : B) (u v : fibf y) : Id (fibf y) u v =\r
+ compId (fibf y) u (fe.1 y) v (<i> fe.2 y u @ -i) (fe.2 y v)\r
+ pc : prop center = propPi B fibf fibprop\r
+ pisc (s : center) (g h : isCenter s) : Id (isCenter s) g h =\r
+ <i> \ (y : B) (w : fibf y) ->\r
+ propSet (fibf y) (fibprop y) (s y) w (g y w) (h y w) @ i\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
+\r
+-- The identity function is an equivalence\r
+idCenter (A : U) (y : A) : fiber A A (idfun A) y = (y, refl A y)\r
+\r
+-- TODO: redifine fiber so this gets nicer?\r
+idIsCenter (A : U) (y : A) (w : fiber A A (idfun A) y)\r
+ : Id (fiber A A (idfun A) y) (idCenter A y) w =\r
+ <i> (w.2 @ -i, <j> w.2 @ j \/ -i)\r
+\r
+idIsEquiv (A : U) : isEquiv A A (idfun A) = (idCenter A,idIsCenter A)\r
+\r
+idEquiv (A : U) : equiv A A = (idfun A, idIsEquiv A)\r
+\r
+-- Transport is an equivalence\r
+-- NB: The proof is taken from the output of a comp U\r
+trans (A B : U) (p : Id U A B) (a : A) : B = transport p a\r
+\r
+transCenter (A B : U) (p : Id U A B) (y : B) : fiber A B (trans A B p) y =\r
+ (comp (<i0> p @ -i0) y []\r
+ ,<i0> comp p (comp (<i0> p @ -i0) y [])\r
+ [ (i0 = 0) -> <i1> comp (<i2> p @ (i1 /\ i2)) (comp (<i0> p @ -i0) y [])\r
+ [ (i1 = 0) -> <i2> comp (<i0> p @ -i0) y [] ]\r
+ , (i0 = 1) -> <i1> comp (<i2> p @ (i1 \/ -i2)) y [ (i1 = 1) -> <i2> y ] ])\r
+\r
+transIsCenter (A B : U) (p : Id U A B) (y : B) (w : fiber A B (trans A B p) y)\r
+ : Id (fiber A B (trans A B p) y) (transCenter A B p y) w\r
+ = <i0>\r
+ ( comp (<i1> p @ -i1) (w.2 @ -i0)\r
+ [ (i0 = 0) -> <i1> comp (<i2> p @ (-i1 \/ -i2)) y [ (i1 = 0) -> <i2> y ]\r
+ , (i0 = 1) -> <i1> comp (<i2> p @ (-i1 /\ i2)) (w.1) [ (i1 = 1) -> <i2> w.1 ] ]\r
+ , <i1> comp (<i2> p @ i2)\r
+ (comp (<i2> p @ -i2) (w.2 @ (-i0 \/ i1))\r
+ [ (i0 = 0) -> <i2> comp (<i3> p @ (-i2 \/ -i3)) y [ (i2 = 0) -> <i3> y ]\r
+ , (i0 = 1)(i1 = 0) ->\r
+ <i2> comp (<i3> p @ (-i2 /\ i3)) (w.1)\r
+ [ (i2 = 1) -> <i3> w.1 ]\r
+ , (i1 = 1) -> <i2> comp (<i3> p @ (-i2 \/ -i3)) y [ (i2 = 0) -> <i3> y ] ])\r
+ [ (i0 = 0) -> <i2> comp (<i3> p @ (i2 /\ i3))\r
+ (comp (<i0> p @ -i0) y [ ])\r
+ [ (i1 = 0) ->\r
+ <i3> comp (<i4> p @ (i2 /\ i3 /\ i4))\r
+ (comp (<i0> p @ -i0) y [ ])\r
+ [ (i2 = 0) -> <i4> comp (<i0> p @ -i0) y [ ]\r
+ , (i3 = 0) -> <i4> comp (<i0> p @ -i0) y [ ] ]\r
+ , (i1 = 1) ->\r
+ <i3> comp (<i4> p @ ((i2 /\ i3) \/ -i4)) y\r
+ [ (i2 = 1)(i3 = 1) -> <i4> y ]\r
+ , (i2 = 0) -> <i3> comp (<i0> p @ -i0) y [ ] ]\r
+ , (i0 = 1) ->\r
+ <i2> comp (<i3> p @ (i2 \/ -i3)) (w.2 @ i1)\r
+ [ (i1 = 0) ->\r
+ <i3> comp (<i4> p @ ((i2 /\ i4) \/ (-i3 /\ i4))) (w.1)\r
+ [ (i2 = 0)(i3 = 1) -> <i4> w.1 ]\r
+ , (i1 = 1) ->\r
+ <i3> comp (<i4> p @ (i2 \/ -i3 \/ -i4)) y\r
+ [ (i2 = 1) -> <i4> y, (i3 = 0) -> <i4> y ]\r
+ , (i2 = 1) -> <i3> w.2 @ i1 ]\r
+ , (i1 = 0) ->\r
+ <i2> comp (<i3> p @ (i2 /\ i3))\r
+ (comp (<i1> p @ -i1) (w.2 @ -i0)\r
+ [ (i0 = 0) ->\r
+ <i1> comp (<i2> p @ (-i1 \/ -i2)) y [ (i1 = 0) -> <i2> y ]\r
+ , (i0 = 1) ->\r
+ <i1> comp (<i2> p @ (-i1 /\ i2)) (w.1)\r
+ [ (i1 = 1) -> <i2> w.1 ]\r
+ ])\r
+ [ (i2 = 0) ->\r
+ <i3> comp (<i1> p @ -i1) (w.2 @ -i0)\r
+ [ (i0 = 0) ->\r
+ <i1> comp (<i2> p @ (-i1 \/ -i2)) y\r
+ [ (i1 = 0) -> <i2> y ]\r
+ , (i0 = 1) ->\r
+ <i1> comp (<i2> p @ (-i1 /\ i2)) (w.1)\r
+ [ (i1 = 1) -> <i2> w.1 ]\r
+ ]\r
+ ]\r
+ , (i1 = 1) -> <i2> comp (<i3> p @ (i2 \/ -i3)) y [ (i2 = 1) -> <i3> y ] ]\r
+ )\r
+\r
+transIsEquiv (A B : U) (p : Id U A B) : isEquiv A B (trans A B p) =\r
+ (transCenter A B p,transIsCenter A B p)\r
+\r
+transEquiv (A B : U) (p : Id U A B) : equiv A B =\r
+ (trans A B p,transIsEquiv A B p)\r
+\r
+transDelta (A : U) : equiv A A = transEquiv A A (<_> A)\r
+\r
+\r
+invEquiv (A B : U) (f : A -> B) (is : isEquiv A B f) (y : B) : A = (is.1 y).1\r
+\r
+invEq (A B : U) (f : equiv A B) : B -> A = invEquiv A B f.1 f.2\r
+\r
+\r
+retEquiv (A B : U) (f : A -> B) (is : isEquiv A B f) (y : B) :\r
+ Id B (f (invEquiv A B f is y)) y = (is.1 y).2\r
+\r
+retEq (A B : U) (f:equiv A B) : (y:B) -> Id B (f.1 (invEq A B f y)) y =\r
+ retEquiv A B f.1 f.2\r
+\r
+secEquiv (A B : U) (f : A -> B) (is : isEquiv A B f) (x : A) :\r
+ Id A (invEquiv A B f is (f x)) x = <i> (is.2 (f x) (x, <_> f x) @ i).1\r
+\r
+secEq (A B : U) (f: equiv A B) : (x:A) -> Id A (invEq A B f (f.1 x)) x =\r
+ secEquiv A B f.1 f.2\r
+\r
+\r
+-- Alternative definition:\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
+\r
+\r
+\r
+-- Another alternative definitions:\r
+\r
+-- isContr (A : U) : U = and (prop A) A\r
+\r
+-- fiber (A B:U) (f:A->B) (b:B) : U = (x:A) * Id B b (f x)\r
+\r
+-- lemIdFib (A:U) (a:A) : prop (fiber A A (\ (x:A) -> x) a) = rem\r
+-- where F : U = fiber A A (\ (x:A) -> x) a\r
+-- rem (u v:F) : Id F u v = <i>(rem1 @ i,rem2 @ i)\r
+-- where x : A = u.1\r
+-- p : Id A a x = u.2\r
+-- y : A = v.1\r
+-- q : Id A a y = v.2\r
+-- rem1 : Id A x y = <i>comp A a [(i=0) -> p,(i=1) -> q]\r
+-- rem2 : IdP (<i>Id A a (rem1@i)) p q = <i j>comp A a [(i=0) -> <l>p@(j/\l),(i=1) -> <l>q@(j/\l)]\r
+\r
+-- lemPropAnd (A B :U) (pA: prop A) (pB: A -> prop B) : prop (and A B) = \r
+-- \ (u v:and A B) -> <i>((pA u.1 v.1)@i, (pB u.1 u.2 v.2)@i)\r
+\r
+-- isContrProp (A:U) : prop (isContr A) = \r
+-- lemPropAnd (prop A) A (propIsProp A) (\ (h:prop A) -> h)\r
+\r
+-- isEquiv (A B:U) (f:A->B) : U = (y:B) -> isContr (fiber A B f y)\r
+\r
+-- idIsEquiv (A:U) : isEquiv A A (idfun A) = \ (a:A) -> (lemIdFib A a,(a,refl A a))\r
+\r
+-- propIsEquiv (A B : U) (f : A -> B) : prop (isEquiv A B f)\r
+-- = propPi B (\ (y:B) -> isContr (fiber A B f y)) (\ (y:B) -> isContrProp (fiber A B f y))\r
+\r
+-- isEquivEq (A B : U) (f : A -> B) (is:isEquiv A B f) : Id U A B = \r
+-- isoId A B f g (\ (y:B) -> <i>(s y)@-i) t\r
+-- where\r
+-- rem1 (y:B) : prop (fiber A B f y) = (is y).1\r
+-- rem2 (y:B) : fiber A B f y = (is y).2\r
+-- g (y:B) : A = (rem2 y).1\r
+-- s (y:B) : Id B y (f (g y)) = (rem2 y).2\r
+-- rem3 (x:A) : Id B (f x) (f (g (f x))) = s (f x)\r
+-- rem4 (x:A) : Id (fiber A B f (f x)) (g (f x),rem3 x) (x,refl B (f x)) = \r
+-- rem1 (f x) (g (f x),rem3 x) (x,refl B (f x))\r
+-- t (x:A) : Id A (g (f x)) x = <i> ((rem4 x)@i).1\r
+ \r
+-- Equiv (A B : U) : U = (f : A -> B) * isEquiv A B f\r
+\r
+-- lemIdEquiv (A B:U) (f g : Equiv A B) (h:Id (A->B) f.1 g.1) : Id (Equiv A B) f g\r
+-- = <i>(h@i,(lemPropF (A->B) (isEquiv A B) (propIsEquiv A B) f.1 g.1 h f.2 g.2)@i)\r
+\r
+-- -- a general lemma about equivalence and fibrations\r
+\r
+-- Sigma (A:U) (F:A->U) : U = (x:A) * F x\r
+\r
+-- lemEquivFib (A:U) (F G :A -> U) (f:(x:A) -> F x -> G x)\r
+-- (h : isEquiv (Sigma A F) (Sigma A G) (\ (xp : Sigma A F) -> (xp.1,f xp.1 xp.2))) (x:A) (v:G x) : \r
+-- isContr (fiber (F x) (G x) (f x) v) = (rem7,psi (rem1.2))\r
+-- where\r
+-- AF : U = Sigma A F\r
+-- AG : U = Sigma A G\r
+-- g (xp : AF) : AG = (xp.1,f xp.1 xp.2)\r
+-- rem1 : isContr (fiber AF AG g (x,v)) = h (x,v)\r
+-- phi (z:fiber (F x) (G x) (f x) v) : fiber AF AG g (x,v) = ((x,z.1),<i>(x,(z.2)@ i))\r
+-- psi (z:fiber AF AG g (x,v)) : fiber (F x) (G x) (f x) v = transport (<i> (u : F (p@-i)) * IdP (<j>G (p@-i /\ j)) v (f (p@-i) u)) (w,q)\r
+-- where yu : AF = z.1\r
+-- y : A = yu.1\r
+-- w : F y = yu.2\r
+-- p : Id A x y = <i>(z.2 @ i).1\r
+-- q : IdP (<j>G (p@j)) v (f y w) = <i>((z.2) @ i).2\r
+-- rem7 (z0 z1 : fiber (F x) (G x) (f x) v) : Id (fiber (F x) (G x) (f x) v) z0 z1 = <i>psi ((rem1.1 (phi z0) (phi z1))@i)\r
+\r
+-- This file contains a proof of the graduate lemma using the old
+-- version of equivalence
module gradLemma where
import equiv
+-- The old version of univalence using the old definition of equivalences
module univalence where
import gradLemma
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) ]
+ <i> 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)
projects / cubicaltt.git / commitdiff