module torsor where\r
+import prelude\r
import circle\r
+import univalence\r
+\r
+setPi (A : U) (B : A -> U) (h : (x : A) -> set (B x))\r
+ (f0 f1 : (x : A) -> B x)\r
+ (p1 p2 : Id ((x : A) -> B x) f0 f1)\r
+ : Id (Id ((x : A) -> B x) f0 f1) p1 p2\r
+ = <i j> \(x : A) -> (h x (f0 x) (f1 x) (<i> (p1@i) x) (<i> (p2@i) x)) @ i @ j\r
+\r
+lemIdPProp (A B : U) (AProp : prop A) (p : Id U A B) : (x : A) -> (y : B) -> IdP p x y\r
+ = J U A (\(B : U) -> \(p : Id U A B) -> (x : A) -> (y : B) -> IdP p x y) AProp B p\r
+\r
+lemIdPSet (A B : U) (ASet : set A) (p : Id U A B) : (x : A) (y : B) (s t : IdP p x y) -> Id (IdP p x y) s t\r
+ = J U A (\(B : U) -> \(p : Id U A B) -> (x : A) (y : B) (s t : IdP p x y) -> Id (IdP p x y) s t) ASet B p\r
+\r
+lemIdPSet2 (A B : U) (ASet : set A) (p1 : Id U A B)\r
+ : (p2 : Id U A B) -> (p : Id (Id U A B) p1 p2) ->\r
+ (x : A) -> (y : B) -> (s : IdP p1 x y) -> (t : IdP p2 x y) -> IdP (<i> (IdP (p @ i) x y)) s t\r
+ = J (Id U A B) p1 (\(p2 : Id U A B) -> \(p : Id (Id U A B) p1 p2) -> (x : A) -> (y : B) -> (s : IdP p1 x y) -> (t : IdP p2 x y) -> IdP (<i> (IdP (p @ i) x y)) s t)\r
+ (lemIdPSet A B ASet p1)\r
+\r
+\r
+isEquivId (A : U) : isEquiv A A (\(x : A) -> x) = gradLemma A A (\(x : A) -> x) (\(x : A) -> x) (\(x : A) -> <_> x) (\(x : A) -> <_> x)\r
+\r
+lem10 (A B : U) (e : equiv A B) (x y : B) (p : Id A (e.2 x).1.1 (e.2 y).1.1) : Id B x y\r
+ = transport\r
+ (compId U (Id B (e.1 (e.2 x).1.1) (e.1 (e.2 y).1.1)) (Id B x (e.1 (e.2 y).1.1)) (Id B x y)\r
+ (<i> Id B (retEq A B e x @ i) (e.1 (e.2 y).1.1)) (<i> Id B x (retEq A B e y @ i)))\r
+ (mapOnPath A B e.1 (e.2 x).1.1 (e.2 y).1.1 p)\r
+\r
+lem10' (A B : U) (e : equiv A B) (x y : A) (p : Id B (e.1 x) (e.1 y)) : Id A x y\r
+ = transport\r
+ (compId U (Id A (e.2 (e.1 x)).1.1 (e.2 (e.1 y)).1.1) (Id A x (e.2 (e.1 y)).1.1) (Id A x y)\r
+ (<i> Id A (secEq A B e x @ i) (e.2 (e.1 y)).1.1) (<i> Id A x (secEq A B e y @ i))\r
+ )\r
+ (mapOnPath B A (invEq A B e) (e.1 x) (e.1 y) p)\r
+\r
+\r
+transRefl (A : U) (a : A) : Id A (transport (<_> A) a) a = <i> comp (<_> A) a [(i=1) -> <_>a]\r
+\r
+lem11 (A : U) : Id (Id U A A) (univalence A A (\(x : A) -> x, isEquivId A)).1.1 (<_> A) = hole\r
+ where\r
+ hole0 : Id (equiv A A)\r
+ (\(x : A) -> x, isEquivId A)\r
+ (transEquiv' A A (<_> A))\r
+ = <i> ( (transRefl (A->A) (\(x : A) -> x) @ -i)\r
+ , lemIdPProp (isEquiv A A (\(x : A) -> x)) (isEquiv A A (transEquiv' A A (<_> A)).1)\r
+ (propIsEquiv A A (\(x : A) -> x)) (<j> isEquiv A A (transRefl (A->A) (\(x : A) -> x) @ -j))\r
+ (isEquivId A) (transEquiv' A A (<_> A)).2 @ i\r
+ )\r
+ hole1 : Id (equiv A A) (transEquiv' A A (univalence A A (\(x : A) -> x, isEquivId A)).1.1) (\(x : A) -> x, isEquivId A)\r
+ = retEq (Id U A A) (equiv A A) (corrUniv' A A) (\(x : A) -> x, isEquivId A)\r
+ hole : Id (Id U A A) (univalence A A (\(x : A) -> x, isEquivId A)).1.1 (<_> A)\r
+ = lem10' (Id U A A) (equiv A A) (corrUniv' A A)\r
+ (univalence A A (\(x : A) -> x, isEquivId A)).1.1 (<_> A)\r
+ (compId (equiv A A) (transEquiv' A A (univalence A A (\(x : A) -> x, isEquivId A)).1.1) (\(x : A) -> x, isEquivId A) (transEquiv' A A (<_> A)) hole1 hole0)\r
+\r
+substIdP (A B : U) (p : Id U A B) (x : A) (y : B) (q : Id B (transport p x) y) : IdP p x y\r
+ = transport (<i> IdP p x (q@i)) hole\r
+ where\r
+ hole : IdP p x (transport p x) = <i> comp (<j> p @ (i /\ j)) x [(i=0) -> <_> x]\r
\r
lemIdSig (A:U) (B : A -> U) (t u : Sigma A B) :\r
Id U (Id (Sigma A B) t u) ((p : Id A t.1 u.1) * IdP (<i> B (p @ i)) t.2 u.2) =\r
hinhpr (X : U) : X -> (ishinh X).1 =\r
\(x : X) (P : hProp) (f : X -> P.1) -> f x\r
\r
+inhPropContr (A : U) (x : prop A) (y : ishinh_UU A) : isContr A = y (isContr A, propIsContr A) (\(z : A) -> (z, x z))\r
+\r
--\r
\r
--- A : U = undefined\r
--- B : U = undefined\r
--- F : A -> B = undefined\r
+P1 (A B : U) (F : A -> B) : U = (x y : A) -> isEquiv (Id A x y) (Id B (F x) (F y)) (mapOnPath A B F x y)\r
+P2 (A B : U) (F : A -> B) : U = (x : A) -> isContr ((y : A) * Id B (F x) (F y))\r
+P3 (A B : U) (F : A -> B) : U = (x : B) -> prop ((y : A) * Id B x (F y))\r
+\r
+propP1 (A B : U) (F : A -> B) : prop (P1 A B F)\r
+ = propPi A (\(x : A) -> (y : A) -> isEquiv (Id A x y) (Id B (F x) (F y)) (mapOnPath A B F x y))\r
+ (\(x : A) -> propPi A (\(y : A) -> isEquiv (Id A x y) (Id B (F x) (F y)) (mapOnPath A B F x y))\r
+ (\(y : A) -> propIsEquiv (Id A x y) (Id B (F x) (F y)) (mapOnPath A B F x y)))\r
\r
--- P1 : U = (x y : A) -> isEquiv (Id A x y) (Id B (F x) (F y)) (mapOnPath A B F x y)\r
--- P2 : U = (x : A) -> isContr ((y : A) * Id B (F x) (F y))\r
--- P3 : U = (x : B) -> prop ((y : A) * Id B x (F y))\r
+propP2 (A B : U) (F : A -> B) : prop (P2 A B F)\r
+ = propPi A (\(x : A) -> isContr ((y : A) * Id B (F x) (F y)))\r
+ (\(x : A) -> propIsContr ((y : A) * Id B (F x) (F y)))\r
\r
--- propP1 : prop P1 = propPi A (\(x : A) -> (y : A) -> isEquiv (Id A x y) (Id B (F x) (F y)) (mapOnPath A B F x y))\r
--- (\(x : A) -> propPi A (\(y : A) -> isEquiv (Id A x y) (Id B (F x) (F y)) (mapOnPath A B F x y))\r
--- (\(y : A) -> propIsEquiv (Id A x y) (Id B (F x) (F y)) (mapOnPath A B F x y)))\r
+propP3 (A B : U) (F : A -> B) : prop (P3 A B F)\r
+ = propPi B (\(x : B) -> prop ((y : A) * Id B x (F y)))\r
+ (\(x : B) -> propIsProp ((y : A) * Id B x (F y)))\r
\r
--- propP2 : prop P2 = propPi A (\(x : A) -> isContr ((y : A) * Id B (F x) (F y)))\r
--- (\(x : A) -> propIsContr ((y : A) * Id B (F x) (F y)))\r
+isoIdProp (A B : U) (AProp : prop A) (BProp : prop B) (F : A -> B) (G : B -> A) : Id U A B =\r
+ isoId A B F G (\(y : B) -> BProp (F (G y)) y) (\(x : A) -> AProp (G (F x)) x)\r
\r
--- propP3 : prop P3 = propPi B (\(x : B) -> prop ((y : A) * Id B x (F y)))\r
--- (\(x : B) -> propIsProp ((y : A) * Id B x (F y)))\r
+equivProp (A B : U) (AProp : prop A) (BProp : prop B) (F : A -> B) (G : B -> A) : equiv A B =\r
+ (F, gradLemma A B F G (\(y : B) -> BProp (F (G y)) y) (\(x : A) -> AProp (G (F x)) x))\r
\r
--- isoIdProp (A B : U) (AProp : prop A) (BProp : prop B) (F : A -> B) (G : B -> A) : Id U A B =\r
--- isoId A B F G (\(y : B) -> BProp (F (G y)) y) (\(x : A) -> AProp (G (F x)) x)\r
+isContrProp (A : U) (p : isContr A) (x y : A) : Id A x y = compId A x p.1 y (<i> p.2 x @ -i) (p.2 y)\r
\r
--- equivProp (A B : U) (AProp : prop A) (BProp : prop B) (F : A -> B) (G : B -> A) : equiv A B =\r
--- (F, gradLemma A B F G (\(y : B) -> BProp (F (G y)) y) (\(x : A) -> AProp (G (F x)) x))\r
+lem2 (A : U) (x : A) : isContr ((y : A) * Id A x y)\r
+ = ( (x, refl A x)\r
+ , \(z : (y : A) * Id A x y) ->\r
+ J A x (\(y : A) -> \(p : Id A x y) -> Id ((y : A) * Id A x y) (x, refl A x) (y, p))\r
+ (refl ((y : A) * Id A x y) (x, refl A x)) z.1 z.2\r
+ )\r
\r
--- isContrProp (A : U) (p : isContr A) (x y : A) : Id A x y = compId A x p.1 y (<i> p.2 x @ -i) (p.2 y)\r
+lem31192 (A : U) (P : A -> U) (aC : isContr A) : Id U (Sigma A P) (P aC.1) =\r
+ isoId (Sigma A P) (P aC.1) F G FG GF\r
+ where\r
+ F (a : Sigma A P) : P aC.1 = transport (<i> P ((aC.2 a.1) @ -i)) a.2\r
+ G (a : P aC.1) : Sigma A P = (aC.1, a)\r
+ FG (a : P aC.1) : Id (P aC.1) (transport (<i> P ((aC.2 aC.1) @ -i)) a) a = hole\r
+ where\r
+ prf : Id (Id A aC.1 aC.1) (aC.2 aC.1) (<_> aC.1) = propSet A (isContrProp A aC) aC.1 aC.1 (aC.2 aC.1) (<_> aC.1)\r
+ hole1 : Id (P aC.1) (transport (<_> P aC.1) a) a = transRefl (P aC.1) a\r
+ hole : Id (P aC.1) (transport (<i> P ((aC.2 aC.1) @ -i)) a) a\r
+ = transport (<i> Id (P aC.1) (transport (<j> P ((prf @ -i) @ -j)) a) a) hole1\r
+ GF (a : Sigma A P) : Id (Sigma A P) (aC.1, transport (<i> P ((aC.2 a.1) @ -i)) a.2) a = hole\r
+ where\r
+ hole2 : Id A aC.1 a.1 = aC.2 a.1\r
+ hole1 : IdP (<i> P (hole2 @ i)) (transport (<i> P ((aC.2 a.1) @ -i)) a.2) a.2\r
+ = <i> comp (<j> P (hole2 @ i \/ -j)) a.2 [(i=1) -> <_> a.2]\r
+ hole : Id (Sigma A P) (aC.1, transport (<i> P ((aC.2 a.1) @ -i)) a.2) a\r
+ = transport (<i> (lemIdSig A P (aC.1, transport (<i> P ((aC.2 a.1) @ -i)) a.2) a) @ -i) (hole2, hole1)\r
\r
--- lem3 (A : U) (x : A) (z : (y : A) * Id A x y) : Id ((y : A) * Id A x y) (x, refl A x) z\r
--- = J A x (\(y : A) -> \(p : Id A x y) -> Id ((y : A) * Id A x y) (x, refl A x) (y, p)) (refl ((y : A) * Id A x y) (x, refl A x)) z.1 z.2\r
--- lem2 (A : U) (x : A) : isContr ((y : A) * Id A x y) = ((x, refl A x), lem3 A x)\r
+total (A : U) (P Q : A -> U) (f : (x : A) -> P x -> Q x) (a : (x : A) * P x) : (x : A) * Q x = (a.1, f a.1 a.2)\r
\r
-transRefl (A : U) (a : A) : Id A (transport (<_> A) a) a = <i> comp (<_> A) a [(i=1) -> <_>a]\r
+ex210 (A : U) (B : A -> U) (C : (x : A) -> B x -> U) : Id U ((x : A) * (y : B x) * C x y) ((x : Sigma A B) * C x.1 x.2)\r
+ = isoId ((x : A) * (y : B x) * C x y) ((x : Sigma A B) * C x.1 x.2) F G FG GF\r
+ where\r
+ F (a : (x : A) * (y : B x) * C x y) : ((x : Sigma A B) * C x.1 x.2) = ((a.1, a.2.1), a.2.2)\r
+ G (a : (x : Sigma A B) * C x.1 x.2) : ((x : A) * (y : B x) * C x y) = (a.1.1, (a.1.2, a.2))\r
+ FG (a : (x : Sigma A B) * C x.1 x.2) : Id ((x : Sigma A B) * C x.1 x.2) (F (G a)) a = <_> a\r
+ GF (a : (x : A) * (y : B x) * C x y) : Id ((x : A) * (y : B x) * C x y) (G (F a)) a = <_> a\r
+\r
+cSigma (A : U) (B : U) (C : A -> B -> U) : Id U ((x : A) * (y : B) * C x y) ((y : B) * (x : A) * C x y) =\r
+ isoId ((x : A) * (y : B) * C x y) ((y : B) * (x : A) * C x y)\r
+ (\(a : (x : A) * (y : B) * C x y) -> (a.2.1, (a.1, a.2.2)))\r
+ (\(a : (y : B) * (x : A) * C x y) -> (a.2.1, (a.1, a.2.2)))\r
+ (\(a : (y : B) * (x : A) * C x y) -> <_> a)\r
+ (\(a : (x : A) * (y : B) * C x y) -> <_> a)\r
+\r
+th476 (A : U) (P Q : A -> U) (f : (x : A) -> P x -> Q x) (x : A) (v : Q x)\r
+ : Id U (fiber (Sigma A P) (Sigma A Q) (total A P Q f) (x, v)) (fiber (P x) (Q x) (f x) v)\r
+ = hole\r
+ where\r
+ A1 : U = (w : Sigma A P) * Id (Sigma A Q) (x, v) (total A P Q f w)\r
+ A2 : U = (a : A) * (u : P a) * Id (Sigma A Q) (x, v) (a, f a u)\r
+ A3 : U = (a : A) * (u : P a) * (p : Id A x a) * IdP (<i> Q (p @ i)) v (f a u)\r
+ A4 : U = (a : A) * (p : Id A x a) * (u : P a) * IdP (<i> Q (p @ i)) v (f a u)\r
+ A5 : U = (w : (a : A) * Id A x a) * (u : P w.1) * IdP (<i> Q (w.2 @ i)) v (f w.1 u)\r
+ A6 : U = (u : P x) * Id (Q x) v (f x u)\r
+ E12 : Id U A1 A2 = <i> (ex210 A P (\(a : A) -> \(b : P a) -> Id (Sigma A Q) (x, v) (a, f a b))) @ -i\r
+ E23 : Id U A2 A3 = <i> (a : A) * (u : P a) * (lemIdSig A Q (x, v) (a, f a u)) @ i\r
+ E34 : Id U A3 A4 = <i> (a : A) * (cSigma (P a) (Id A x a) (\(u : P a) -> \(p : Id A x a) -> IdP (<j> Q (p @ j)) v (f a u))) @ i\r
+ E45 : Id U A4 A5 = ex210 A (Id A x) (\(a : A) -> \(p : Id A x a) -> (u : P a) * IdP (<i> Q (p @ i)) v (f a u))\r
+ E56 : Id U A5 A6 = lem31192 ((a : A) * Id A x a) (\(w : (a : A) * Id A x a) -> (u : P w.1) * IdP (<i> Q (w.2 @ i)) v (f w.1 u))\r
+ (lem2 A x)\r
+ hole : Id U A1 A6 = compId U A1 A2 A6 E12 (compId U A2 A3 A6 E23 (compId U A3 A4 A6 E34 (compId U A4 A5 A6 E45 E56)))\r
+\r
+thm477 (A : U) (P Q : A -> U) (f : (x : A) -> P x -> Q x)\r
+ : Id U ((x : A) -> isEquiv (P x) (Q x) (f x)) (isEquiv ((x : A) * P x) ((x : A) * Q x) (total A P Q f))\r
+ = hole\r
+ where\r
+ AProp : prop ((x : A) -> isEquiv (P x) (Q x) (f x))\r
+ = propPi A (\(x : A) -> isEquiv (P x) (Q x) (f x)) (\(x : A) -> propIsEquiv (P x) (Q x) (f x))\r
+ BProp : prop (isEquiv ((x : A) * P x) ((x : A) * Q x) (total A P Q f)) = propIsEquiv ((x : A) * P x) ((x : A) * Q x) (total A P Q f)\r
+ F (a : (x : A) -> isEquiv (P x) (Q x) (f x)) (y : (x : A) * Q x) : isContr (fiber (Sigma A P) (Sigma A Q) (total A P Q f) y)\r
+ = transport (<i> isContr (th476 A P Q f y.1 y.2 @ -i)) (a y.1 y.2)\r
+ G (a : isEquiv ((x : A) * P x) ((x : A) * Q x) (total A P Q f)) (x : A) (y : Q x) : isContr (fiber (P x) (Q x) (f x) y)\r
+ = transport (<i> isContr (th476 A P Q f x y @ i)) (a (x, y))\r
+ hole : Id U ((x : A) -> isEquiv (P x) (Q x) (f x)) (isEquiv ((x : A) * P x) ((x : A) * Q x) (total A P Q f))\r
+ = isoIdProp ((x : A) -> isEquiv (P x) (Q x) (f x)) (isEquiv ((x : A) * P x) ((x : A) * Q x) (total A P Q f)) AProp BProp F G\r
+\r
+F12 (A B : U) (F : A -> B) (p1 : P1 A B F) (x : A) : isContr ((y : A) * Id B (F x) (F y)) = hole\r
+ where\r
+ hole3 : ((y : A) * Id A x y) -> ((y : A) * Id B (F x) (F y))\r
+ = total A (\(y : A) -> Id A x y) (\(y : A) -> Id B (F x) (F y)) (mapOnPath A B F x)\r
+ hole2 : isEquiv ((y : A) * Id A x y) ((y : A) * Id B (F x) (F y)) hole3\r
+ = transport (thm477 A (\(y : A) -> Id A x y) (\(y : A) -> Id B (F x) (F y)) (mapOnPath A B F x)) (p1 x)\r
+ hole4 : Id U ((y : A) * Id A x y) ((y : A) * Id B (F x) (F y)) = equivId ((y : A) * Id A x y) ((y : A) * Id B (F x) (F y)) hole3 hole2\r
+ hole : isContr ((y : A) * Id B (F x) (F y)) = transport (<i> isContr (hole4@i)) (lem2 A x)\r
+\r
+contrEquiv (A B : U) (aC : isContr A) (bC : isContr B) : equiv A B\r
+ = (\(_ : A) -> bC.1, gradLemma A B (\(_ : A) -> bC.1) (\(_ : B) -> aC.1) (\(x : B) -> bC.2 x) (\(x : A) -> aC.2 x))\r
\r
--- lem31192 (A : U) (P : A -> U) (aC : isContr A) : Id U (Sigma A P) (P aC.1) =\r
--- isoId (Sigma A P) (P aC.1) F G FG GF\r
--- where\r
--- F (a : Sigma A P) : P aC.1 = transport (<i> P ((aC.2 a.1) @ -i)) a.2\r
--- G (a : P aC.1) : Sigma A P = (aC.1, a)\r
--- FG (a : P aC.1) : Id (P aC.1) (transport (<i> P ((aC.2 aC.1) @ -i)) a) a = hole\r
--- where\r
--- prf : Id (Id A aC.1 aC.1) (aC.2 aC.1) (<_> aC.1) = propSet A (isContrProp A aC) aC.1 aC.1 (aC.2 aC.1) (<_> aC.1)\r
--- hole1 : Id (P aC.1) (transport (<_> P aC.1) a) a = transRefl (P aC.1) a\r
--- hole : Id (P aC.1) (transport (<i> P ((aC.2 aC.1) @ -i)) a) a\r
--- = transport (<i> Id (P aC.1) (transport (<j> P ((prf @ -i) @ -j)) a) a) hole1\r
--- GF (a : Sigma A P) : Id (Sigma A P) (aC.1, transport (<i> P ((aC.2 a.1) @ -i)) a.2) a = hole\r
--- where\r
--- hole2 : Id A aC.1 a.1 = aC.2 a.1\r
--- hole1 : IdP (<i> P (hole2 @ i)) (transport (<i> P ((aC.2 a.1) @ -i)) a.2) a.2\r
--- = <i> comp (<j> P (hole2 @ i \/ -j)) a.2 [(i=1) -> <_> a.2]\r
--- hole : Id (Sigma A P) (aC.1, transport (<i> P ((aC.2 a.1) @ -i)) a.2) a\r
--- = transport (<i> (lemIdSig A P (aC.1, transport (<i> P ((aC.2 a.1) @ -i)) a.2) a) @ -i) (hole2, hole1)\r
-\r
--- total (A : U) (P Q : A -> U) (f : (x : A) -> P x -> Q x) (a : (x : A) * P x) : (x : A) * Q x = (a.1, f a.1 a.2)\r
-\r
--- ex210 (A : U) (B : A -> U) (C : (x : A) -> B x -> U) : Id U ((x : A) * (y : B x) * C x y) ((x : Sigma A B) * C x.1 x.2)\r
--- = isoId ((x : A) * (y : B x) * C x y) ((x : Sigma A B) * C x.1 x.2) F G FG GF\r
--- where\r
--- F (a : (x : A) * (y : B x) * C x y) : ((x : Sigma A B) * C x.1 x.2) = ((a.1, a.2.1), a.2.2)\r
--- G (a : (x : Sigma A B) * C x.1 x.2) : ((x : A) * (y : B x) * C x y) = (a.1.1, (a.1.2, a.2))\r
--- FG (a : (x : Sigma A B) * C x.1 x.2) : Id ((x : Sigma A B) * C x.1 x.2) (F (G a)) a = <_> a\r
--- GF (a : (x : A) * (y : B x) * C x y) : Id ((x : A) * (y : B x) * C x y) (G (F a)) a = <_> a\r
-\r
--- cSigma (A : U) (B : U) (C : A -> B -> U) : Id U ((x : A) * (y : B) * C x y) ((y : B) * (x : A) * C x y) =\r
--- isoId ((x : A) * (y : B) * C x y) ((y : B) * (x : A) * C x y)\r
--- (\(a : (x : A) * (y : B) * C x y) -> (a.2.1, (a.1, a.2.2)))\r
--- (\(a : (y : B) * (x : A) * C x y) -> (a.2.1, (a.1, a.2.2)))\r
--- (\(a : (y : B) * (x : A) * C x y) -> <_> a)\r
--- (\(a : (x : A) * (y : B) * C x y) -> <_> a)\r
-\r
--- th476 (A : U) (P Q : A -> U) (f : (x : A) -> P x -> Q x) (x : A) (v : Q x)\r
--- : Id U (fiber (Sigma A P) (Sigma A Q) (total A P Q f) (x, v)) (fiber (P x) (Q x) (f x) v)\r
--- = hole\r
--- where\r
--- A1 : U = (w : Sigma A P) * Id (Sigma A Q) (x, v) (total A P Q f w)\r
--- A2 : U = (a : A) * (u : P a) * Id (Sigma A Q) (x, v) (a, f a u)\r
--- A3 : U = (a : A) * (u : P a) * (p : Id A x a) * IdP (<i> Q (p @ i)) v (f a u)\r
--- A4 : U = (a : A) * (p : Id A x a) * (u : P a) * IdP (<i> Q (p @ i)) v (f a u)\r
--- A5 : U = (w : (a : A) * Id A x a) * (u : P w.1) * IdP (<i> Q (w.2 @ i)) v (f w.1 u)\r
--- A6 : U = (u : P x) * Id (Q x) v (f x u)\r
--- E12 : Id U A1 A2 = <i> (ex210 A P (\(a : A) -> \(b : P a) -> Id (Sigma A Q) (x, v) (a, f a b))) @ -i\r
--- E23 : Id U A2 A3 = <i> (a : A) * (u : P a) * (lemIdSig A Q (x, v) (a, f a u)) @ i\r
--- E34 : Id U A3 A4 = <i> (a : A) * (cSigma (P a) (Id A x a) (\(u : P a) -> \(p : Id A x a) -> IdP (<j> Q (p @ j)) v (f a u))) @ i\r
--- E45 : Id U A4 A5 = ex210 A (Id A x) (\(a : A) -> \(p : Id A x a) -> (u : P a) * IdP (<i> Q (p @ i)) v (f a u))\r
--- E56 : Id U A5 A6 = lem31192 ((a : A) * Id A x a) (\(w : (a : A) * Id A x a) -> (u : P w.1) * IdP (<i> Q (w.2 @ i)) v (f w.1 u))\r
--- (lem2 A x)\r
--- hole : Id U A1 A6 = compId U A1 A2 A6 E12 (compId U A2 A3 A6 E23 (compId U A3 A4 A6 E34 (compId U A4 A5 A6 E45 E56)))\r
-\r
--- thm477 (A : U) (P Q : A -> U) (f : (x : A) -> P x -> Q x)\r
--- : Id U ((x : A) -> isEquiv (P x) (Q x) (f x)) (isEquiv ((x : A) * P x) ((x : A) * Q x) (total A P Q f))\r
--- = hole\r
--- where\r
--- AProp : prop ((x : A) -> isEquiv (P x) (Q x) (f x))\r
--- = propPi A (\(x : A) -> isEquiv (P x) (Q x) (f x)) (\(x : A) -> propIsEquiv (P x) (Q x) (f x))\r
--- BProp : prop (isEquiv ((x : A) * P x) ((x : A) * Q x) (total A P Q f)) = propIsEquiv ((x : A) * P x) ((x : A) * Q x) (total A P Q f)\r
--- F (a : (x : A) -> isEquiv (P x) (Q x) (f x)) (y : (x : A) * Q x) : isContr (fiber (Sigma A P) (Sigma A Q) (total A P Q f) y)\r
--- = transport (<i> isContr (th476 A P Q f y.1 y.2 @ -i)) (a y.1 y.2)\r
--- G (a : isEquiv ((x : A) * P x) ((x : A) * Q x) (total A P Q f)) (x : A) (y : Q x) : isContr (fiber (P x) (Q x) (f x) y)\r
--- = transport (<i> isContr (th476 A P Q f x y @ i)) (a (x, y))\r
--- hole : Id U ((x : A) -> isEquiv (P x) (Q x) (f x)) (isEquiv ((x : A) * P x) ((x : A) * Q x) (total A P Q f))\r
--- = isoIdProp ((x : A) -> isEquiv (P x) (Q x) (f x)) (isEquiv ((x : A) * P x) ((x : A) * Q x) (total A P Q f)) AProp BProp F G\r
-\r
--- F12 (p1 : P1) (x : A) : isContr ((y : A) * Id B (F x) (F y)) = hole\r
--- where\r
--- hole3 : ((y : A) * Id A x y) -> ((y : A) * Id B (F x) (F y))\r
--- = total A (\(y : A) -> Id A x y) (\(y : A) -> Id B (F x) (F y)) (mapOnPath A B F x)\r
--- hole2 : isEquiv ((y : A) * Id A x y) ((y : A) * Id B (F x) (F y)) hole3\r
--- = transport (thm477 A (\(y : A) -> Id A x y) (\(y : A) -> Id B (F x) (F y)) (mapOnPath A B F x)) (p1 x)\r
--- hole4 : Id U ((y : A) * Id A x y) ((y : A) * Id B (F x) (F y)) = equivId ((y : A) * Id A x y) ((y : A) * Id B (F x) (F y)) hole3 hole2\r
--- hole : isContr ((y : A) * Id B (F x) (F y)) = transport (<i> isContr (hole4@i)) (lem2 A x)\r
-\r
--- contrEquiv (A B : U) (aC : isContr A) (bC : isContr B) : equiv A B\r
--- = (\(_ : A) -> bC.1, gradLemma A B (\(_ : A) -> bC.1) (\(_ : B) -> aC.1) (\(x : B) -> bC.2 x) (\(x : A) -> aC.2 x))\r
-\r
--- F21 (p2 : P2) (x y : A) : isEquiv (Id A x y) (Id B (F x) (F y)) (mapOnPath A B F x y) = hole3 y\r
--- where\r
--- hole0 : ((y : A) * Id A x y) -> ((y : A) * Id B (F x) (F y))\r
--- = total A (\(y : A) -> Id A x y) (\(y : A) -> Id B (F x) (F y)) (mapOnPath A B F x)\r
--- hole2 : isEquiv ((y : A) * Id A x y) ((y : A) * Id B (F x) (F y)) hole0\r
--- = (equivProp ((y : A) * Id A x y) ((y : A) * Id B (F x) (F y))\r
--- (isContrProp ((y : A) * Id A x y) (lem2 A x))\r
--- (isContrProp ((y : A) * Id B (F x) (F y)) (p2 x))\r
--- hole0 (\(_ : (y : A) * Id B (F x) (F y)) -> (x, <_> x))).2\r
--- hole4 : Id U ((y : A) -> isEquiv (Id A x y) (Id B (F x) (F y)) (mapOnPath A B F x y)) (isEquiv ((y : A) * Id A x y) ((y : A) * Id B (F x) (F y)) hole0)\r
--- = thm477 A (\(y : A) -> Id A x y) (\(y : A) -> Id B (F x) (F y)) (mapOnPath A B F x)\r
--- hole3 : (y : A) -> isEquiv (Id A x y) (Id B (F x) (F y)) (mapOnPath A B F x y)\r
--- = transport (<i> hole4 @ -i) hole2\r
-\r
--- F32 (p3 : P3) (x : A) : isContr ((y : A) * Id B (F x) (F y))\r
--- = ((x, refl B (F x)), \(q : ((y : A) * Id B (F x) (F y))) -> p3 (F x) (x, refl B (F x)) q)\r
-\r
--- lemReflComp (A : U) (a b : A) (p : Id A a b) : Id (Id A a b) (compId A a a b (<_> a) p) p =\r
--- <j i> comp (<k> A) (p @ i /\ j) [(i=0) -> <_> a, (j=1) -> <_> p @ i, (i=1) -> <k> p @ k \/ j ]\r
-\r
--- F23 (p2 : P2) (x : B) (a b : (y : A) * Id B x (F y)) : Id ((y : A) * Id B x (F y)) a b = hole\r
--- where\r
--- hole2 : Id ((y : A) * Id B (F a.1) (F y)) (a.1, refl B (F a.1)) (b.1, compId B (F a.1) x (F b.1) (<i> a.2 @ -i) b.2)\r
--- = isContrProp ((y : A) * Id B (F a.1) (F y)) (p2 (a.1)) (a.1, refl B (F a.1)) (b.1, compId B (F a.1) x (F b.1) (<i> a.2 @ -i) b.2)\r
--- hole3 : (Id ((y : A) * Id B x (F y)) a (b.1, compId B x x (F b.1) (<_> x) b.2))\r
--- = transport\r
--- (<i> Id ((y : A) * Id B (a.2 @ -i) (F y)) (a.1, <j> a.2 @ -i \/ j) (b.1, compId B (a.2 @ -i) x (F b.1) (<j> a.2 @ -i /\ -j) b.2))\r
--- hole2\r
--- hole : Id ((y : A) * Id B x (F y)) a b\r
--- = transport\r
--- (<i> Id ((y : A) * Id B x (F y)) a (b.1, (lemReflComp B x (F b.1) b.2) @ i))\r
--- hole3\r
-\r
--- E12 : Id U P1 P2 = isoIdProp P1 P2 propP1 propP2 F12 F21\r
--- E23 : Id U P2 P3 = isoIdProp P2 P3 propP2 propP3 F23 F32\r
+F21 (A B : U) (F : A -> B) (p2 : P2 A B F) (x y : A) : isEquiv (Id A x y) (Id B (F x) (F y)) (mapOnPath A B F x y) = hole3 y\r
+ where\r
+ hole0 : ((y : A) * Id A x y) -> ((y : A) * Id B (F x) (F y))\r
+ = total A (\(y : A) -> Id A x y) (\(y : A) -> Id B (F x) (F y)) (mapOnPath A B F x)\r
+ hole2 : isEquiv ((y : A) * Id A x y) ((y : A) * Id B (F x) (F y)) hole0\r
+ = (equivProp ((y : A) * Id A x y) ((y : A) * Id B (F x) (F y))\r
+ (isContrProp ((y : A) * Id A x y) (lem2 A x))\r
+ (isContrProp ((y : A) * Id B (F x) (F y)) (p2 x))\r
+ hole0 (\(_ : (y : A) * Id B (F x) (F y)) -> (x, <_> x))).2\r
+ hole4 : Id U ((y : A) -> isEquiv (Id A x y) (Id B (F x) (F y)) (mapOnPath A B F x y)) (isEquiv ((y : A) * Id A x y) ((y : A) * Id B (F x) (F y)) hole0)\r
+ = thm477 A (\(y : A) -> Id A x y) (\(y : A) -> Id B (F x) (F y)) (mapOnPath A B F x)\r
+ hole3 : (y : A) -> isEquiv (Id A x y) (Id B (F x) (F y)) (mapOnPath A B F x y)\r
+ = transport (<i> hole4 @ -i) hole2\r
+\r
+F32 (A B : U) (F : A -> B) (p3 : P3 A B F) (x : A) : isContr ((y : A) * Id B (F x) (F y))\r
+ = ((x, refl B (F x)), \(q : ((y : A) * Id B (F x) (F y))) -> p3 (F x) (x, refl B (F x)) q)\r
+\r
+lemReflComp (A : U) (a b : A) (p : Id A a b) : Id (Id A a b) (compId A a a b (<_> a) p) p =\r
+ <j i> comp (<k> A) (p @ i /\ j) [(i=0) -> <_> a, (j=1) -> <_> p @ i, (i=1) -> <k> p @ k \/ j ]\r
+\r
+F23 (A B : U) (F : A -> B) (p2 : P2 A B F) (x : B) (a b : (y : A) * Id B x (F y)) : Id ((y : A) * Id B x (F y)) a b = hole\r
+ where\r
+ hole2 : Id ((y : A) * Id B (F a.1) (F y)) (a.1, refl B (F a.1)) (b.1, compId B (F a.1) x (F b.1) (<i> a.2 @ -i) b.2)\r
+ = isContrProp ((y : A) * Id B (F a.1) (F y)) (p2 (a.1)) (a.1, refl B (F a.1)) (b.1, compId B (F a.1) x (F b.1) (<i> a.2 @ -i) b.2)\r
+ hole3 : (Id ((y : A) * Id B x (F y)) a (b.1, compId B x x (F b.1) (<_> x) b.2))\r
+ = transport\r
+ (<i> Id ((y : A) * Id B (a.2 @ -i) (F y)) (a.1, <j> a.2 @ -i \/ j) (b.1, compId B (a.2 @ -i) x (F b.1) (<j> a.2 @ -i /\ -j) b.2))\r
+ hole2\r
+ hole : Id ((y : A) * Id B x (F y)) a b\r
+ = transport\r
+ (<i> Id ((y : A) * Id B x (F y)) a (b.1, (lemReflComp B x (F b.1) b.2) @ i))\r
+ hole3\r
+\r
+E12 (A B : U) (F : A -> B) : Id U (P1 A B F) (P2 A B F) = isoIdProp (P1 A B F) (P2 A B F) (propP1 A B F) (propP2 A B F) (F12 A B F) (F21 A B F)\r
+E23 (A B : U) (F : A -> B) : Id U (P2 A B F) (P3 A B F) = isoIdProp (P2 A B F) (P3 A B F) (propP2 A B F) (propP3 A B F) (F23 A B F) (F32 A B F)\r
+E13 (A B : U) (F : A -> B) : Id U (P1 A B F) (P3 A B F) = compId U (P1 A B F) (P2 A B F) (P3 A B F) (E12 A B F) (E23 A B F)\r
\r
-- torsor\r
\r
action (A : U) (shift : equiv A A) (x : A) : Z -> A = split\r
- inl n -> actionAux n x\r
- where actionAux : nat -> A -> A = split\r
- zero -> invEq A A shift\r
- suc n -> \(x : A) -> invEq A A shift (actionAux n x)\r
- inr n -> actionAux n x\r
- where actionAux : nat -> A -> A = split\r
- zero -> \(x : A) -> x\r
- suc n -> \(x : A) -> shift.1 (actionAux n x)\r
+ inl n -> invEq A A shift (actionAux n)\r
+ where actionAux : nat -> A = split\r
+ zero -> x\r
+ suc n -> action A shift x (inl n)\r
+ inr n -> actionAux n\r
+ where actionAux : nat -> A = split\r
+ zero -> x\r
+ suc n -> shift.1 (action A shift x (inr n))\r
\r
data BZ = bz (A : U) (ASet : set A) (a : ishinh_UU A)\r
(AShift : equiv A A)\r
BZShift : (A : BZ) -> equiv (BZSet A) (BZSet A) = split\r
bz A ASet a AShift AEquiv -> AShift\r
\r
+BZAction (A : BZ) : BZSet A -> Z -> BZSet A = action (BZSet A) (BZShift A)\r
+\r
BZS (A : BZ) : BZSet A -> BZSet A = (BZShift A).1\r
+BZP (A : BZ) (a : BZSet A) : BZSet A = ((BZShift A).2 a).1.1\r
\r
-BZEquiv : (A : BZ) -> (x : BZSet A) -> isEquiv Z (BZSet A) (action (BZSet A) (BZShift A) x) = split\r
+BZEquiv : (A : BZ) -> (x : BZSet A) -> isEquiv Z (BZSet A) (BZAction A x) = split\r
bz A ASet a AShift AEquiv -> AEquiv\r
\r
-lemIdPProp (A B : U) (AProp : prop A) (p : Id U A B) : (x : A) -> (y : B) -> IdP p x y\r
- = J U A (\(B : U) -> \(p : Id U A B) -> (x : A) -> (y : B) -> IdP p x y) AProp B p\r
-\r
-lemBZ : (BA BB : BZ) -> (p : Id U (BZSet BA) (BZSet BB)) ->\r
- (pS : IdP (<i> p@i -> p@i) (BZS BA) (BZS BB)) -> Id BZ BA BB = split\r
+lemBZ : (BA BB : BZ) ->\r
+ equiv ((p : Id U (BZSet BA) (BZSet BB)) * IdP (<i> p@i -> p@i) (BZS BA) (BZS BB)) (Id BZ BA BB) = split\r
bz A ASet a AShift AEquiv -> hole\r
where\r
BA : BZ = bz A ASet a AShift AEquiv\r
- hole : (BB : BZ) -> (p : Id U (BZSet BA) (BZSet BB)) ->\r
- (pS : IdP (<i> p@i -> p@i) (BZS BA) (BZS BB)) -> Id BZ BA BB = split\r
+ hole : (BB : BZ) ->\r
+ equiv ((p : Id U (BZSet BA) (BZSet BB)) * IdP (<i> p@i -> p@i) (BZS BA) (BZS BB)) (Id BZ BA BB) = split\r
bz B BSet b BShift BEquiv -> hole\r
where\r
BB : BZ = bz B BSet b BShift BEquiv\r
- hole (p : Id U A B) (pS : IdP (<i> p@i -> p@i) (BZS BA) (BZS BB)) : Id BZ BA BB = hole\r
+ F (w : (p : Id U A B) * IdP (<i> p@i -> p@i) (BZS BA) (BZS BB)) : Id BZ BA BB = hole\r
where\r
+ p : Id U A B = w.1\r
+ pS : IdP (<i> p@i -> p@i) (BZS BA) (BZS BB) = w.2\r
pASet : IdP (<i> set (p@i)) ASet BSet\r
= lemIdPProp (set A) (set B) (setIsProp A) (<i> set (p@i)) ASet BSet\r
pNE : IdP (<i> ishinh_UU (p@i)) a b\r
(<i> (x : p@i) -> isEquiv Z (p@i) (action (p@i) (pShift@i) x))\r
AEquiv BEquiv\r
hole : Id BZ BA BB = <i> bz (p@i) (pASet@i) (pNE@i) (pShift@i) (pEquiv@i)\r
-\r
--- negZ : Z -> Z = split\r
--- inl n -> inr (suc n)\r
--- inr n -> negAux n\r
--- where negAux : nat -> Z = split\r
--- zero -> inr zero\r
--- suc n -> inl n\r
+ G (q : Id BZ BA BB) : (p : Id U A B) * IdP (<i> p@i -> p@i) (BZS BA) (BZS BB) = (<i> BZSet (q @ i), <i> (BZShift (q@i)).1)\r
+ GF (w : (p : Id U A B) * IdP (<i> p@i -> p@i) (BZS BA) (BZS BB))\r
+ : Id ((p : Id U A B) * IdP (<i> p@i -> p@i) (BZS BA) (BZS BB)) (<i> BZSet (F w @ i), <i> (BZShift (F w @ i)).1) w\r
+ = <_> w\r
+ FG (q : Id BZ BA BB) : Id (Id BZ BA BB) (F (<i> BZSet (q@i), <i> (BZShift (q@i)).1)) q = hole\r
+ where\r
+ p : Id U A B = <i> BZSet (q@i)\r
+ p2 : IdP (<i> p@i -> p@i) (BZS BA) (BZS BB) = <i> (BZShift (q@i)).1\r
+ q2 : Id BZ BA BB = F (p, p2)\r
+ pASet : Id (IdP (<i> set (p@i)) ASet BSet) (<i> BZASet (q2@i)) (<i> BZASet (q@i))\r
+ = lemIdPSet (set A) (set B) (propSet (set A) (setIsProp A)) (<i> set (p@i)) ASet BSet (<i> BZASet (q2@i)) (<i> BZASet (q@i))\r
+ pNE : Id (IdP (<i> ishinh_UU (p@i)) a b) (<i> BZNE (q2@i)) (<i> BZNE (q@i))\r
+ = lemIdPSet (ishinh_UU A) (ishinh_UU B) (propSet (ishinh_UU A) (propishinh A)) (<i> ishinh_UU (p@i)) a b (<i> BZNE (q2@i)) (<i> BZNE (q@i))\r
+ pShift : Id (IdP (<i> equiv (p@i) (p@i)) AShift BShift) (<i> BZShift (q2@i)) (<i> BZShift (q@i)) =\r
+ <j i> ( p2 @ i\r
+ , (lemIdPSet\r
+ (isEquiv A A AShift.1)\r
+ (isEquiv B B BShift.1)\r
+ (propSet (isEquiv A A AShift.1) (propIsEquiv A A AShift.1))\r
+ (<i> isEquiv (p@i) (p@i) (p2@i))\r
+ AShift.2 BShift.2\r
+ (<i> (BZShift (q2@i)).2) (<i> (BZShift (q@i)).2)) @ j @ i\r
+ )\r
+ pEquiv : IdP (<j> IdP (<i> (x : p@i) -> isEquiv Z (p@i) (action (p@i) (pShift@j@i) x)) AEquiv BEquiv) (<i> BZEquiv (q2@i)) (<i> BZEquiv (q@i))\r
+ = lemIdPSet2\r
+ ((x : A) -> isEquiv Z A (action A AShift x))\r
+ ((x : B) -> isEquiv Z B (action B BShift x))\r
+ (propSet ((x : A) -> isEquiv Z A (action A AShift x))\r
+ (propPi A (\(x : A) -> isEquiv Z A (action A AShift x))\r
+ (\(x : A) -> propIsEquiv Z A (action A AShift x))))\r
+ (<i> (x : p@i) -> isEquiv Z (p@i) (action (p@i) (pShift@0@i) x))\r
+ (<i> (x : p@i) -> isEquiv Z (p@i) (action (p@i) (pShift@1@i) x))\r
+ (<j i> (x : p@i) -> isEquiv Z (p@i) (action (p@i) (pShift@j@i) x))\r
+ AEquiv BEquiv (<i> BZEquiv (q2@i)) (<i> BZEquiv (q@i))\r
+ hole0 : Id (Id BZ BA BB) q2 (<i> bz (BZSet (q @ i)) (BZASet (q @ i)) (BZNE (q @ i)) (BZShift (q @ i)) (BZEquiv (q @ i)))\r
+ = <j i> bz (p@i) (pASet@j@i) (pNE@j@i) (pShift@j@i) (pEquiv@j@i)\r
+ hole1 : Id (Id BZ BA BB) (<i> bz (BZSet (q @ i)) (BZASet (q @ i)) (BZNE (q @ i)) (BZShift (q @ i)) (BZEquiv (q @ i))) q\r
+ = undefined\r
+ hole : Id (Id BZ BA BB) q2 q = compId (Id BZ BA BB) q2 (<i> bz (BZSet (q @ i)) (BZASet (q @ i)) (BZNE (q @ i)) (BZShift (q @ i)) (BZEquiv (q @ i))) q hole0 hole1\r
+ hole : equiv ((p : Id U (BZSet BA) (BZSet BB)) * IdP (<i> p@i -> p@i) (BZS BA) (BZS BB)) (Id BZ BA BB)\r
+ = (F, gradLemma ((p : Id U (BZSet BA) (BZSet BB)) * IdP (<i> p@i -> p@i) (BZS BA) (BZS BB)) (Id BZ BA BB) F G FG GF)\r
+\r
+transConstN (A : U) (a : A) : (n : nat) -> A = split\r
+ zero -> a\r
+ suc n -> transport (<_> A) (transConstN A a n)\r
+\r
+transConstNRefl (A : U) (a : A) : (n : nat) -> Id A (transConstN A a n) a = split\r
+ zero -> <_> a\r
+ suc n -> compId A (transport (<_> A) (transConstN A a n)) (transConstN A a n) a\r
+ (transRefl A (transConst N A a n)) (transConstNRefl A a n)\r
+\r
+lem0 (A B : U) (f : A -> B) (e : isEquiv A B f) (x : A)\r
+ : Id B (transport (univalence B A (f, e)).1.1 x) (f x)\r
+ = transConstNRefl B (f x) (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))))))\r
+\r
+lem1 (A B : U) (f : A -> B) (e : isEquiv A B f) (x : B)\r
+ : Id A (transport (<i> (univalence B A (f, e)).1.1 @ -i) x) (e x).1.1\r
+ = compId A\r
+ (transConstN A (e (transConstN B x (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))))).1.1 (suc (suc (suc zero))))\r
+ (transConstN A (e x).1.1 (suc (suc (suc zero))))\r
+ (e x).1.1\r
+ (<i> transConstN A (e (transConstNRefl B x (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))) @ i)).1.1 (suc (suc (suc zero))))\r
+ (transConstNRefl A (e x).1.1 (suc (suc (suc zero))))\r
+\r
+lem2 (A : BZ) (a : BZSet A) : (x : Z) -> Id (BZSet A) (BZS A (BZAction A a x)) (BZAction A a (sucZ x)) = split\r
+ inl n -> lem2Aux n\r
+ where\r
+ lem2Aux : (n : nat) -> Id (BZSet A) (BZS A (BZAction A a (inl n))) (BZAction A a (sucZ (inl n))) = split\r
+ zero -> retEq (BZSet A) (BZSet A) (BZShift A) a\r
+ suc n -> retEq (BZSet A) (BZSet A) (BZShift A) (BZAction A a (inl n))\r
+ inr n -> lem2Aux n\r
+ where\r
+ lem2Aux : (n : nat) -> Id (BZSet A) (BZS A (BZAction A a (inr n))) (BZAction A a (sucZ (inr n))) = split\r
+ zero -> <_> BZS A a\r
+ suc n -> <_> BZS A (BZAction A a (inr (suc n)))\r
\r
ZBZ : BZ = bz Z ZSet (hinhpr Z zeroZ) ZShift ZEquiv\r
where\r
ZShift : equiv Z Z = (sucZ, gradLemma Z Z sucZ predZ sucpredZ predsucZ)\r
ZEquiv (x : Z) : isEquiv Z Z (action Z ZShift x) = hole\r
where\r
- lem (x y : Z) : Id Z (action Z ZShift x (sucZ y)) (sucZ (action Z ZShift x y)) = undefined\r
hole : isEquiv Z Z (action Z ZShift x) = undefined\r
\r
-lem5 (A B : U) (p : Id U A B) (a : A) (b : B) (q : Id B (transport p a) b) : IdP p a b = undefined\r
+-- action (A : U) (shift : equiv A A) (x : A) : Z -> A = split\r
+-- inl n -> invEq A A shift (actionAux n)\r
+-- where actionAux : nat -> A = split\r
+-- zero -> x\r
+-- suc n -> action A shift x (inl n)\r
+-- inr n -> actionAux n\r
+-- where actionAux : nat -> A = split\r
+-- zero -> x\r
+-- suc n -> shift.1 (action A shift x (inr n))\r
\r
-loopZ : Id BZ ZBZ ZBZ = lemBZ ZBZ ZBZ sucIdZ q\r
+\r
+prf : Id (equiv Z Z) (BZAction ZBZ zeroZ, BZEquiv ZBZ zeroZ) (\(x : Z) -> x, isEquivId Z)\r
+ = hole\r
+ where\r
+ hole0 : (x : Z) -> Id Z (BZAction ZBZ zeroZ x) x = split\r
+ inl n -> hole1 n\r
+ where\r
+ hole1 : (n : nat) -> Id Z (BZAction ZBZ zeroZ (inl n)) (inl n) = split\r
+ zero -> <_> inl zero\r
+ suc n -> mapOnPath Z Z predZ (BZAction ZBZ zeroZ (inl n)) (inl n) (hole1 n)\r
+ inr n -> hole1 n\r
+ where\r
+ hole1 : (n : nat) -> Id Z (BZAction ZBZ zeroZ (inr n)) (inr n) = split\r
+ zero -> <_> inr zero\r
+ suc n -> mapOnPath Z Z sucZ (BZAction ZBZ zeroZ (inr n)) (inr n) (hole1 n)\r
+ hole : Id (equiv Z Z) (BZAction ZBZ zeroZ, BZEquiv ZBZ zeroZ) (\(x : Z) -> x, isEquivId Z)\r
+ = <i> (\(x : Z) -> hole0 x @ i,\r
+ lemIdPProp\r
+ (isEquiv Z Z (BZAction ZBZ zeroZ)) (isEquiv Z Z (\(x : Z) -> x))\r
+ (propIsEquiv Z Z (BZAction ZBZ zeroZ))\r
+ (<j> isEquiv Z Z (\(x : Z) -> hole0 x @ j))\r
+ (BZEquiv ZBZ zeroZ) (isEquivId Z) @ i\r
+ )\r
+\r
+transportIsoId (A B : U) (f : A -> B) (g : B -> A)\r
+ (s : (y : B) -> Id B (f (g y)) y)\r
+ (t : (x : A) -> Id A (g (f x)) x)\r
+ (x : A)\r
+ : Id B (transport (isoId A B f g s t) x) (f x)\r
+ = compId B (transport (<_> B) (transport (<_> B) (f x))) (transport (<_> B) (f x)) (f x)\r
+ (<i> transport (<_> B) (transRefl B (f x) @ i)) (transRefl B (f x))\r
+\r
+transportIsoId' (A B : U) (f : A -> B) (g : B -> A)\r
+ (s : (y : B) -> Id B (f (g y)) y)\r
+ (t : (x : A) -> Id A (g (f x)) x)\r
+ (x : B)\r
+ : Id A (transport (<i> isoId A B f g s t @ -i) x) (g x)\r
+ = compId A (transport (<_> A) (g (transport (<_> B) x))) (transport (<_> A) (g x)) (g x)\r
+ (<i> transport (<_> A) (g (transRefl B x @ i))) (transRefl A (g x))\r
+\r
+loopZ : Id BZ ZBZ ZBZ = (lemBZ ZBZ ZBZ).1 (sucIdZ, hole)\r
where\r
- q : IdP (<i> (sucIdZ@i) -> (sucIdZ@i)) sucZ sucZ = undefined\r
- hole : U = U\r
+ hole1 (x : Z) : Id Z (transport sucIdZ (sucZ (transport (<j> sucIdZ @ -j) x))) (sucZ (sucZ (predZ x))) =\r
+ compId Z (transport sucIdZ (sucZ (transport (<j> sucIdZ @ -j) x))) (transport sucIdZ (sucZ (predZ x))) (sucZ (sucZ (predZ x)))\r
+ (<i> transport sucIdZ (sucZ (transportIsoId' Z Z sucZ predZ sucpredZ predsucZ x @ i))) (transportIsoId Z Z sucZ predZ sucpredZ predsucZ (sucZ (predZ x)))\r
+ hole2 (x : Z) : Id Z (sucZ (sucZ (predZ x))) (sucZ x) = <i> sucZ (sucpredZ x @ i)\r
+ hole3 : Id (Z->Z) (transport (<i> (sucIdZ@i) -> (sucIdZ@i)) sucZ) sucZ\r
+ = <i> \(x : Z) -> compId Z (transport sucIdZ (sucZ (transport (<j> sucIdZ @ -j) x))) (sucZ (sucZ (predZ x))) (sucZ x)\r
+ (hole1 x) (hole2 x) @ i\r
+ hole : IdP (<i> (sucIdZ@i) -> (sucIdZ@i)) sucZ sucZ = substIdP (Z->Z) (Z->Z) (<i> (sucIdZ@i) -> (sucIdZ@i)) sucZ sucZ hole3\r
\r
F : S1 -> BZ = split\r
base -> ZBZ\r
loop @ i -> loopZ @ i\r
\r
+encode (A : BZ) (p : Id BZ ZBZ A) : BZSet A = transport (<i> BZSet (p@i)) zeroZ\r
+\r
+decode (A : BZ) (a : BZSet A) : Id BZ ZBZ A = (lemBZ ZBZ A).1 (<i> p @ -i, <i> q @ -i)\r
+ where\r
+ p1 : isEquiv Z (BZSet A) (BZAction A a) = BZEquiv A a\r
+ p : Id U (BZSet A) Z = <i> (univalence (BZSet A) Z (BZAction A a, p1)).1.1 @ -i\r
+ hole1 (x : Z) : Id Z (transport p (BZS A (transport (<i> p @ -i) x)))\r
+ (p1 (BZS A (BZAction A a x))).1.1\r
+ = compId Z (transport p (BZS A (transport (<i> p @ -i) x)))\r
+ (transport p (BZS A (BZAction A a x)))\r
+ (p1 (BZS A (BZAction A a x))).1.1\r
+ (<i> transport p (BZS A (lem0 Z (BZSet A) (BZAction A a) p1 x @ i)))\r
+ (lem1 Z (BZSet A) (BZAction A a) p1 (BZS A (BZAction A a x)))\r
+ hole2 (x : Z) : Id Z (p1 (BZS A (BZAction A a x))).1.1 (sucZ x)\r
+ = compId Z (p1 (BZS A (BZAction A a x))).1.1 (p1 (BZAction A a (sucZ x))).1.1 (sucZ x)\r
+ (<i> (p1 (lem2 A a x @ i)).1.1)\r
+ (secEq Z (BZSet A) (BZAction A a, p1) (sucZ x))\r
+ hole : Id (Z->Z) (\(x : Z) -> transport p (BZS A (transport (<i> p @ -i) x))) sucZ\r
+ = <i> \(x : Z) -> compId Z (transport p (BZS A (transport (<i> p @ -i) x))) (p1 (BZS A (BZAction A a x))).1.1 (sucZ x)\r
+ (hole1 x) (hole2 x) @ i\r
+ q : IdP (<i> (p@i) -> (p@i)) (BZS A) sucZ = substIdP (BZSet A -> BZSet A) (Z -> Z) (<i> (p@i) -> (p@i)) (BZS A) sucZ hole\r
+\r
LoopsZBZ : Id U (Id BZ ZBZ ZBZ) Z = isoId (Id BZ ZBZ ZBZ) Z (encode ZBZ) (decode ZBZ) (encodeDecode ZBZ) (decodeEncode ZBZ)\r
where\r
- encode (A : BZ) (p : Id BZ ZBZ A) : BZSet A = transport (<i> BZSet (p@i)) zeroZ\r
- decode (A : BZ) (x : BZSet A) : Id BZ ZBZ A = lemBZ ZBZ A p q\r
- where\r
- p : Id U Z (BZSet A) = equivId Z (BZSet A) (action (BZSet A) (BZShift A) x) (BZEquiv A x)\r
- q : IdP (<i> (p@i) -> (p@i)) sucZ (BZS A) = undefined\r
- decodeEncodeRefl : Id (Id BZ ZBZ ZBZ) (decode ZBZ zeroZ) (<_> ZBZ) = undefined\r
+ decodeEncodeRefl0\r
+ : Id (Id U Z Z) (univalence Z Z (BZAction ZBZ zeroZ, BZEquiv ZBZ zeroZ)).1.1 (<_> Z)\r
+ = transport (<i> Id (Id U Z Z) (univalence Z Z (prf @ -i)).1.1 (<_> Z)) (lem11 Z)\r
+ decodeEncodeRefl1\r
+ : IdP (<j> (IdP (<i> decodeEncodeRefl0@j@i -> decodeEncodeRefl0@j@i) sucZ sucZ))\r
+ (<i> (BZShift (decode ZBZ zeroZ@i)).1) (<_> sucZ)\r
+ = lemIdPSet2 (Z->Z) (Z->Z) (setPi Z (\(_ : Z) -> Z) (\(_ : Z) -> ZSet))\r
+ (<j> decodeEncodeRefl0@0@j -> decodeEncodeRefl0@0@j)\r
+ (<j> decodeEncodeRefl0@1@j -> decodeEncodeRefl0@1@j)\r
+ (<i j> decodeEncodeRefl0@i@j -> decodeEncodeRefl0@i@j)\r
+ sucZ sucZ (<i> (BZShift (decode ZBZ zeroZ@i)).1) (<_> sucZ)\r
+ decodeEncodeRefl2 : Id ((p : Id U Z Z) * IdP (<i> p@i -> p@i) sucZ sucZ) ((lemBZ ZBZ ZBZ).2 (decode ZBZ zeroZ)).1.1 ((lemBZ ZBZ ZBZ).2 (<_> ZBZ)).1.1\r
+ = <i> (decodeEncodeRefl0 @ i, decodeEncodeRefl1 @ i)\r
+ decodeEncodeRefl : Id (Id BZ ZBZ ZBZ) (decode ZBZ zeroZ) (<_> ZBZ)\r
+ = lem10 ((p : Id U Z Z) * IdP (<i> p@i -> p@i) sucZ sucZ) (Id BZ ZBZ ZBZ) (lemBZ ZBZ ZBZ) (decode ZBZ zeroZ) (<_> ZBZ) decodeEncodeRefl2\r
decodeEncode : (A : BZ) -> (p : Id BZ ZBZ A) -> Id (Id BZ ZBZ A) (decode A (encode A p)) p\r
= J BZ ZBZ (\(A : BZ) -> \(p : Id BZ ZBZ A) -> Id (Id BZ ZBZ A) (decode A (encode A p)) p) decodeEncodeRefl\r
- encodeDecode (A : BZ) (p : BZSet A) : Id (BZSet A) (transport (<_> BZSet A) (transport (<_> BZSet A) p)) p\r
- = compId (BZSet A) (transport (<_> BZSet A) (transport (<_> BZSet A) p)) (transport (<_> BZSet A) p) p\r
- (<i> transport (<_> BZSet A) (transRefl (BZSet A) p @ i)) (transRefl (BZSet A) p)\r
+ encodeDecode (A : BZ) (p : BZSet A) : Id (BZSet A) (transport (univalence (BZSet A) Z (BZAction A p, BZEquiv A p)).1.1 zeroZ) p\r
+ = lem0 Z (BZSet A) (BZAction A p) (BZEquiv A p) zeroZ\r
+\r
+F_fullyFaithful (x y : S1) : isEquiv (Id S1 x y) (Id BZ (F x) (F y)) (mapOnPath S1 BZ F x y)\r
+ = hole\r
+ where\r
+ hole : isEquiv (Id S1 x y) (Id BZ (F x) (F y)) (mapOnPath S1 BZ F x y) = undefined\r
\r
-F_fullyFaithful (x y : S1) : isEquiv (Id S1 x y) (Id BZ (F x) (F y)) (mapOnPath S1 BZ F x y) = undefined\r
\r
F_essentiallySurjective (y : BZ) : (x : S1) * Id BZ y (F x) = hole\r
where\r
- hInh : ishinh_UU ((x : S1) * Id BZ y (F x)) = undefined\r
- hProp : prop ((x : S1) * Id BZ y (F x)) = undefined\r
- hContr : isContr ((x : S1) * Id BZ y (F x)) = undefined\r
+ hInh : (y : BZ) -> ishinh_UU ((x : S1) * Id BZ y (F x)) = split\r
+ bz A ASet a AShift AEquiv -> hole\r
+ where\r
+ y : BZ = bz A ASet a AShift AEquiv\r
+ hole2 (a : A) : (x : S1) * Id BZ y (F x) = (base, <i> decode y a @ -i)\r
+ hole1 (a : A) : ishinh_UU ((x : S1) * Id BZ y (F x)) = hinhpr ((x : S1) * Id BZ y (F x)) (hole2 a)\r
+ hole : ishinh_UU ((x : S1) * Id BZ y (F x)) = a (ishinh_UU ((x : S1) * Id BZ y (F x)), propishinh ((x : S1) * Id BZ y (F x))) hole1\r
+ hProp : prop ((x : S1) * Id BZ y (F x)) = transport (E13 S1 BZ F) (F_fullyFaithful) y\r
+ hContr : isContr ((x : S1) * Id BZ y (F x)) = inhPropContr ((x : S1) * Id BZ y (F x)) hProp (hInh y)\r
hole : (x : S1) * Id BZ y (F x) = hContr.1\r
+\r
+-- -- tensor (x y : BZ) : BZ = hole\r
+-- -- where\r
+-- -- Z : U = Id BZ x y\r
+-- -- ZSet : set Z = undefined\r
+-- -- z : ishinh_UU Z = undefined\r
+-- -- ZShift : equiv Z Z = undefined\r
+-- -- hole : BZ = undefined\r
projects / cubicaltt.git / commitdiff