module torsor where\r
import prelude\r
+import int\r
import circle\r
+import helix\r
import univalence\r
\r
+lemEquiv1 (A B : U) (F : A -> B) (G : A -> B) (e : isEquiv A B G) (p : (x : A) -> Id A (e (F x)).1.1 x) : Id (A -> B) F G\r
+ = <i> \(x : A) -> transport (<i> Id B (retEq A B (G, e) (F x) @ i) (G x)) (mapOnPath A B G (e (F x)).1.1 x (p x)) @ i\r
+\r
+transRefl (A : U) (a : A) : Id A (transport (<_> A) a) a = <i> comp (<_> A) a [(i=1) -> <_>a]\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
+lemReflComp' (A : U) (a b : A) (p : Id A a b) : Id (Id A a b) (compId A a b b p (<_> b)) p =\r
+ <j i> comp (<k> A) (p @ i) [(i=0) -> <_> a, (j=1) -> <_> p @ i, (i=1) -> <_> b ]\r
+\r
+transportCompId (a b c : U) (p1 : Id U a b) (p2 : Id U b c) (x : a)\r
+ : Id c (transport (compId U a b c p1 p2) x) (transport p2 (transport p1 x))\r
+ = J U b (\(c : U) -> \(p2 : Id U b c) -> Id c (comp (compId U a b c p1 p2) x []) (comp p2 (transport p1 x) []))\r
+ hole c p2\r
+ where\r
+ hole : Id b (comp (compId U a b b p1 (<_> b)) x []) (comp (<_> b) (transport p1 x) []) =\r
+ compId b (comp (compId U a b b p1 (<_> b)) x []) (transport p1 x) (comp (<_> b) (transport p1 x) [])\r
+ (<i> comp (lemReflComp' U a b p1 @ i) x [])\r
+ (<i> transRefl b (transport p1 x) @ -i)\r
+\r
+lemRevCompId (A : U) (a b c : A) (p1 : Id A a b) (p2 : Id A b c)\r
+ : Id (Id A c a) (<i> compId A a b c p1 p2 @ -i) (compId A c b a (<i> p2@-i) (<i> p1@-i))\r
+ = <j i> comp (<k> A) (hole1 @ i @ j) [(i=0) -> <k> p2 @ k \/ j, (i=1) -> <k> p1 @ -k /\ j]\r
+ where\r
+ hole1 : Square A b a c b (<i> p1@-i) (<i> p2@-i) p2 p1\r
+ = <i j> comp (<k> A) (p1 @ -i \/ j) [(i=0) -> <k> p2 @ j /\ k, (i=1) -> <_> p1@j, (j=0) -> <_> p1@-i, (j=1) -> <k> p2 @ k /\ -i ]\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
(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
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
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
- (AEquiv : (x : A) -> isEquiv Z A (action A AShift x))\r
+BZ : U = (A : U) * (ASet : set A) * (a : ishinh_UU A)\r
+ * (AShift : equiv A A)\r
+ * ( (x : A) -> isEquiv Z A (action A AShift x))\r
\r
-BZSet : BZ -> U = split\r
- bz A ASet a AShift AEquiv -> A\r
+BZSet (x : BZ) : U = x.1\r
\r
-BZASet : (A : BZ) -> set (BZSet A) = split\r
- bz A ASet a AShift AEquiv -> ASet\r
+BZASet (A : BZ) : set (BZSet A) = A.2.1\r
\r
-BZNE : (A : BZ) -> ishinh_UU (BZSet A) = split\r
- bz A ASet a AShift AEquiv -> a\r
+BZNE (A : BZ) : ishinh_UU (BZSet A) = A.2.2.1\r
\r
-BZShift : (A : BZ) -> equiv (BZSet A) (BZSet A) = split\r
- bz A ASet a AShift AEquiv -> AShift\r
+BZShift (A : BZ) : equiv (BZSet A) (BZSet A) = A.2.2.2.1\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) (BZAction A x) = split\r
- bz A ASet a AShift AEquiv -> AEquiv\r
+BZEquiv (A : BZ) : (x : BZSet A) -> isEquiv Z (BZSet A) (BZAction A x) = A.2.2.2.2\r
\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
+lemBZ (BA BB : BZ) : equiv ((p : Id U (BZSet BA) (BZSet BB)) * IdP (<i> p@i -> p@i) (BZS BA) (BZS BB)) (Id BZ BA BB) = hole\r
where\r
- BA : BZ = bz A ASet a AShift AEquiv\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
- 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
- = lemIdPProp (ishinh_UU A) (ishinh_UU B) (propishinh A) (<i> ishinh_UU (p@i)) a b\r
- pShift : IdP (<i> equiv (p@i) (p@i)) AShift BShift =\r
- <i> ( pS @ i\r
- , (lemIdPProp\r
- (isEquiv A A AShift.1)\r
- (isEquiv B B BShift.1)\r
- (propIsEquiv A A AShift.1)\r
- (<j> isEquiv (p@j) (p@j) (pS@j))\r
- AShift.2 BShift.2) @ i\r
- )\r
- pEquiv : IdP (<i> (x : p@i) -> isEquiv Z (p@i) (action (p@i) (pShift@i) x)) AEquiv BEquiv\r
- = lemIdPProp\r
- ((x : A) -> isEquiv Z A (action A AShift x))\r
- ((x : B) -> isEquiv Z B (action B BShift 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@i) x))\r
- AEquiv BEquiv\r
- hole : Id BZ BA BB = <i> bz (p@i) (pASet@i) (pNE@i) (pShift@i) (pEquiv@i)\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
+ A : U = BA.1\r
+ ASet : set A = BA.2.1\r
+ a : ishinh_UU A = BA.2.2.1\r
+ AShift : equiv A A = BA.2.2.2.1\r
+ AEquiv : (x : A) -> isEquiv Z A (BZAction BA x) = BA.2.2.2.2\r
+\r
+ B : U = BB.1\r
+ BSet : set B = BB.2.1\r
+ b : ishinh_UU B = BB.2.2.1\r
+ BShift : equiv B B = BB.2.2.2.1\r
+ BEquiv : (x : B) -> isEquiv Z B (BZAction BB x) = BB.2.2.2.2\r
+\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
+ = lemIdPProp (ishinh_UU A) (ishinh_UU B) (propishinh A) (<i> ishinh_UU (p@i)) a b\r
+ pShift : IdP (<i> equiv (p@i) (p@i)) AShift BShift =\r
+ <i> ( pS @ i\r
+ , (lemIdPProp\r
+ (isEquiv A A AShift.1)\r
+ (isEquiv B B BShift.1)\r
+ (propIsEquiv A A AShift.1)\r
+ (<j> isEquiv (p@j) (p@j) (pS@j))\r
+ AShift.2 BShift.2) @ i\r
+ )\r
+ pEquiv : IdP (<i> (x : p@i) -> isEquiv Z (p@i) (action (p@i) (pShift@i) x)) AEquiv BEquiv\r
+ = lemIdPProp\r
+ ((x : A) -> isEquiv Z A (action A AShift x))\r
+ ((x : B) -> isEquiv Z B (action B BShift 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@i) x))\r
+ AEquiv BEquiv\r
+ hole : Id BZ BA BB = <i> (p@i, (pASet@i, (pNE@i, (pShift@i, pEquiv@i))))\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
+ hole : Id (Id BZ BA BB) q2 q = <j i> (p@i, (pASet@j@i, (pNE@j@i, (pShift@j@i, pEquiv@j@i))))\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
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
+ (transRefl A (transConstN 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
(<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
+lem2 (A : U) (shift : equiv A A) (a : A) : (x : Z) -> Id A (shift.1 (action A shift a x)) (action A shift 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
+ lem2Aux : (n : nat) -> Id A (shift.1 (action A shift a (inl n))) (action A shift a (sucZ (inl n))) = split\r
+ zero -> retEq A A shift a\r
+ suc n -> retEq A A shift (action A shift 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
+ lem2Aux : (n : nat) -> Id A (shift.1 (action A shift a (inr n))) (action A shift a (sucZ (inr n))) = split\r
+ zero -> <_> shift.1 a\r
+ suc n -> <_> shift.1 (action A shift a (inr (suc n)))\r
\r
-ZBZ : BZ = bz Z ZSet (hinhpr Z zeroZ) ZShift ZEquiv\r
+lem2' (A : U) (shift : equiv A A) (a : A) : (x : Z) -> Id A (shift.2 (action A shift a x)).1.1 (action A shift a (predZ x)) = split\r
+ inl n -> lem2Aux n\r
+ where\r
+ lem2Aux : (n : nat) -> Id A (shift.2 (action A shift a (inl n))).1.1 (action A shift a (predZ (inl n))) = split\r
+ zero -> <_> action A shift a (predZ (inl zero))\r
+ suc n -> <_> action A shift a (predZ (inl (suc n)))\r
+ inr n -> lem2Aux n\r
+ where\r
+ lem2Aux : (n : nat) -> Id A (shift.2 (action A shift a (inr n))).1.1 (action A shift a (predZ (inr n))) = split\r
+ zero -> <_> action A shift a (inl zero)\r
+ suc n -> secEq A A shift (action A shift a (inr n))\r
+\r
+negZ : Z -> Z = split\r
+ inl u -> inr (suc u)\r
+ inr u -> hole u\r
+ where\r
+ hole : nat -> Z = split\r
+ zero -> inr zero\r
+ suc n -> inl n\r
+\r
+negNegZ : (x : Z) -> Id Z (negZ (negZ x)) x = split\r
+ inl u -> <_> inl u\r
+ inr u -> hole u\r
+ where\r
+ hole : (n : nat) -> Id Z (negZ (negZ (inr n))) (inr n) = split\r
+ zero -> <_> inr zero\r
+ suc n -> <_> inr (suc n)\r
+\r
+ZBZ : 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
+ plus : Z -> Z -> Z = action Z ZShift\r
+ plusCommZero : (y : Z) -> Id Z (plus zeroZ y) (plus y zeroZ) = undefined\r
+ plusComm : (x y : Z) -> Id Z (plus x y) (plus y x) = undefined\r
+ plusNeg : (x : Z) -> Id Z (plus (negZ x) x) zeroZ = split\r
+ inl u -> hole u\r
+ where\r
+ hole : (n : nat) -> Id Z (plus (inr (suc n)) (inl n)) zeroZ = split\r
+ zero -> <_> zeroZ\r
+ suc n -> hole2\r
+ where\r
+ hole2 : Id Z (predZ (plus (inr (suc (suc n))) (inl n))) zeroZ = undefined\r
+ inr u -> hole u\r
+ where\r
+ hole : (n : nat) -> Id Z (plus (negZ (inr n)) (inr n)) zeroZ = split\r
+ zero -> <_> zeroZ\r
+ suc n -> hole2\r
+ where\r
+ hole2 : Id Z (plus (inl n) (inr (suc n))) zeroZ = undefined\r
+\r
+ plusAssoc (x y : Z) : (z : Z) -> Id Z (plus (plus x y) z) (plus x (plus y z)) = split\r
+ inl u -> hole u\r
+ where\r
+ hole : (n : nat) -> Id Z (plus (plus x y) (inl n)) (plus x (plus y (inl n))) = split\r
+ zero -> lem2' Z ZShift x y\r
+ suc n -> compId Z (predZ (plus (plus x y) (inl n))) (predZ (plus x (plus y (inl n)))) (plus x (predZ (plus y (inl n))))\r
+ (<i> predZ (plusAssoc x y (inl n) @ i)) (lem2' Z ZShift x (plus y (inl n)))\r
+ inr u -> hole u\r
+ where\r
+ hole : (n : nat) -> Id Z (plus (plus x y) (inr n)) (plus x (plus y (inr n))) = split\r
+ zero -> <_> plus x y\r
+ suc n -> hole3\r
+ where hole3 : Id Z (sucZ (plus (plus x y) (inr n))) (plus x (sucZ (plus y (inr n))))\r
+ = compId Z (sucZ (plus (plus x y) (inr n))) (sucZ (plus x (plus y (inr n)))) (plus x (sucZ (plus y (inr n))))\r
+ (<i> sucZ (plusAssoc x y (inr n) @ i)) (lem2 Z ZShift x (plus y (inr n)))\r
+ ZEquiv (x : Z) : isEquiv Z Z (plus x) = hole\r
where\r
- hole : isEquiv Z Z (action Z ZShift x) = undefined\r
-\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
+ G : Z -> Z = plus (negZ x)\r
+ FG (a : Z) : Id Z (plus x (plus (negZ x) a)) a = undefined\r
+ GF (a : Z) : Id Z (plus (negZ x) (plus x a)) a = undefined\r
+ hole : isEquiv Z Z (plus x) = undefined\r
\r
+loopBZ : U = Id BZ ZBZ ZBZ\r
+compBZ : loopBZ -> loopBZ -> loopBZ = compId BZ ZBZ ZBZ ZBZ\r
\r
prf : Id (equiv Z Z) (BZAction ZBZ zeroZ, BZEquiv ZBZ zeroZ) (\(x : Z) -> x, isEquivId Z)\r
= hole\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
+loopZ : loopBZ = (lemBZ ZBZ ZBZ).1 (sucIdZ, hole)\r
where\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
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
+encodeZ (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
+decodeZ (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
- 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 (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
+ -- 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 (BZSet A) (BZShift 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\r
+ = undefined\r
+ -- = substIdP (BZSet A -> BZSet A) (Z -> Z) (<i> (p@i) -> (p@i)) (BZS A) sucZ hole\r
+\r
+-- decodeEncodeZRefl0\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
+-- decodeEncodeZRefl1\r
+-- : IdP (<j> (IdP (<i> decodeEncodeZRefl0@j@i -> decodeEncodeZRefl0@j@i) sucZ sucZ))\r
+-- (<i> (BZShift (decodeZ ZBZ zeroZ@i)).1) (<_> sucZ)\r
+-- = lemIdPSet2 (Z->Z) (Z->Z) (setPi Z (\(_ : Z) -> Z) (\(_ : Z) -> ZSet))\r
+-- (<j> decodeEncodeZRefl0@0@j -> decodeEncodeZRefl0@0@j)\r
+-- (<j> decodeEncodeZRefl0@1@j -> decodeEncodeZRefl0@1@j)\r
+-- (<i j> decodeEncodeZRefl0@i@j -> decodeEncodeZRefl0@i@j)\r
+-- sucZ sucZ (<i> (BZShift (decodeZ ZBZ zeroZ@i)).1) (<_> sucZ)\r
+-- decodeEncodeZRefl2 : Id ((p : Id U Z Z) * IdP (<i> p@i -> p@i) sucZ sucZ) ((lemBZ ZBZ ZBZ).2 (decodeZ ZBZ zeroZ)).1.1 ((lemBZ ZBZ ZBZ).2 (<_> ZBZ)).1.1\r
+-- = <i> (decodeEncodeZRefl0 @ i, decodeEncodeZRefl1 @ i)\r
+-- decodeEncodeZRefl : Id loopBZ (decodeZ ZBZ zeroZ) (<_> ZBZ)\r
+-- = lem10 ((p : Id U Z Z) * IdP (<i> p@i -> p@i) sucZ sucZ) loopBZ (lemBZ ZBZ ZBZ) (decodeZ ZBZ zeroZ) (<_> ZBZ) decodeEncodeZRefl2\r
+\r
+decodeEncodeZ : (A : BZ) -> (p : Id BZ ZBZ A) -> Id (Id BZ ZBZ A) (decodeZ A (encodeZ A p)) p\r
+ = undefined\r
+-- = J BZ ZBZ (\(A : BZ) -> \(p : Id BZ ZBZ A) -> Id (Id BZ ZBZ A) (decodeZ A (encodeZ A p)) p) decodeEncodeZRefl\r
+encodeDecodeZ (A : BZ) (p : BZSet A) : Id (BZSet A) (transport (univalence (BZSet A) Z (BZAction A p, BZEquiv A p)).1.1 zeroZ) p\r
+ = undefined\r
+-- = lem0 Z (BZSet A) (BZAction A p) (BZEquiv A p) zeroZ\r
+\r
+----\r
+\r
+loopBZequalsZ : Id U loopBZ Z = isoId loopBZ Z (encodeZ ZBZ) (decodeZ ZBZ) (encodeDecodeZ ZBZ) (decodeEncodeZ ZBZ)\r
+\r
+loopS1equalsLoopBZ : Id U loopS1 loopBZ = compId U loopS1 Z loopBZ loopS1equalsZ (<i> loopBZequalsZ @ -i)\r
+loopS1equalsLoopBZ' : equiv loopS1 loopBZ = transEquiv' loopBZ loopS1 loopS1equalsLoopBZ\r
+\r
+\r
+G : (y : S1) -> Id BZ ZBZ (F y) -> Id S1 base y = split\r
+ base -> \(x : Id BZ ZBZ ZBZ) -> (loopS1equalsLoopBZ'.2 x).1.1\r
+ loop @ i -> hole @ i\r
+ where\r
+ hole1 : Id (loopBZ -> loopS1)\r
+ (\(x : Id BZ ZBZ ZBZ) -> compS1 ((loopS1equalsLoopBZ'.2 (compBZ x (<i> loopZ @ -i))).1.1) loop1)\r
+ (\(x : Id BZ ZBZ ZBZ) -> (loopS1equalsLoopBZ'.2 x).1.1)\r
+ = undefined\r
+ hole : IdP (<i> Id BZ ZBZ (F (loop1 @ i)) -> Id S1 base (loop1 @ i))\r
+ (\(x : Id BZ ZBZ ZBZ) -> (loopS1equalsLoopBZ'.2 x).1.1)\r
+ (\(x : Id BZ ZBZ ZBZ) -> (loopS1equalsLoopBZ'.2 x).1.1)\r
+ = substIdP (loopBZ -> loopS1) (loopBZ -> loopS1)\r
+ (<i> Id BZ ZBZ (F (loop1 @ i)) -> Id S1 base (loop1 @ i))\r
+ (\(x : Id BZ ZBZ ZBZ) -> (loopS1equalsLoopBZ'.2 x).1.1)\r
+ (\(x : Id BZ ZBZ ZBZ) -> (loopS1equalsLoopBZ'.2 x).1.1)\r
+ hole1\r
+\r
+GF : (y : S1) -> (x : Id S1 base y) -> Id (Id S1 base y) (G y (mapOnPath S1 BZ F base y x)) x\r
+ = J S1 base (\(y : S1) -> \(x : Id S1 base y) -> Id (Id S1 base y) (G y (mapOnPath S1 BZ F base y x)) x)\r
+ hole\r
+ where\r
+ hole1 : Id loopS1 (<i> comp (<_>S1) base [(i=0)-><_>base,(i=1)-><_>base]) (<_> base)\r
+ = <j i> comp (<_>S1) base [(i=0)-><_>base,(j=1)-><_>base,(i=1)-><_>base]\r
+ hole : Id loopS1\r
+ (<i> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base [(i=0)-><_>base,(i=1)-><_>base]) [(i=0)-><_>base,(i=1)-><_>base]) [(i=0)-><_>base,(i=1)-><_>base]) (<_> base)\r
+ = compId loopS1\r
+ (<i> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base [(i=0)-><_>base,(i=1)-><_>base]) [(i=0)-><_>base,(i=1)-><_>base]) [(i=0)-><_>base,(i=1)-><_>base])\r
+ (<i> comp (<_>S1) (comp (<_>S1) base [(i=0)-><_>base,(i=1)-><_>base]) [(i=0)-><_>base,(i=1)-><_>base])\r
+ (<_> base)\r
+ (<j i> comp (<_>S1) (comp (<_>S1) (hole1@j@i) [(i=0)-><_>base,(i=1)-><_>base]) [(i=0)-><_>base,(i=1)-><_>base])\r
+ (compId loopS1\r
+ (<i> comp (<_>S1) (comp (<_>S1) base [(i=0)-><_>base,(i=1)-><_>base]) [(i=0)-><_>base,(i=1)-><_>base])\r
+ (<i> comp (<_>S1) base [(i=0)-><_>base,(i=1)-><_>base])\r
+ (<_> base)\r
+ (<j i> comp (<_>S1) (hole1@j@i) [(i=0)-><_>base,(i=1)-><_>base])\r
+ hole1)\r
+\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
+ = lemPropFib (\(x : S1) -> (y : S1) -> isEquiv (Id S1 x y) (Id BZ (F x) (F y)) (mapOnPath S1 BZ F x y))\r
+ (\(x : S1) -> propPi S1 (\(y : S1) -> isEquiv (Id S1 x y) (Id BZ (F x) (F y)) (mapOnPath S1 BZ F x y))\r
+ (\(y : S1) -> propIsEquiv (Id S1 x y) (Id BZ (F x) (F y)) (mapOnPath S1 BZ F x y)))\r
+ (lemPropFib (\(y : S1) -> isEquiv (Id S1 base y) (Id BZ ZBZ (F y)) (mapOnPath S1 BZ F base y))\r
+ (\(y : S1) -> propIsEquiv (Id S1 base y) (Id BZ ZBZ (F y)) (mapOnPath S1 BZ F base 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
+ -- hole0 : Id (loopS1 -> loopBZ) (mapOnPath S1 BZ F base base) loopS1equalsLoopBZ'.1\r
+ -- = lemEquiv1 loopS1 loopBZ (mapOnPath S1 BZ F base base) loopS1equalsLoopBZ'.1 loopS1equalsLoopBZ'.2 (GF base)\r
+ hole : isEquiv loopS1 loopBZ (mapOnPath S1 BZ F base base)\r
+ = undefined\r
+ -- = transport (<i> isEquiv loopS1 loopBZ (hole0 @ -i)) loopS1equalsLoopBZ'.2\r
\r
F_essentiallySurjective (y : BZ) : (x : S1) * Id BZ y (F x) = hole\r
where\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
+ hInh (y : BZ) : ishinh_UU ((x : S1) * Id BZ y (F x)) = hole\r
+ where\r
+ hole2 (a : BZSet y) : (x : S1) * Id BZ y (F x) = (base, <i> decodeZ y a @ -i)\r
+ hole1 (a : BZSet y) : 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)) = BZNE y (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
+S1equalsBZ : Id U S1 BZ = hole\r
+ where\r
+ G (y : BZ) : S1 = (F_essentiallySurjective y).1\r
+ FG (y : BZ) : Id BZ (F (G y)) y = <i> (F_essentiallySurjective y).2 @ -i\r
+ GF (x : S1) : Id S1 (G (F x)) x = (F_fullyFaithful (G (F x)) x (FG (F x))).1.1\r
+ hole : Id U S1 BZ = isoId S1 BZ F G FG GF\r
projects / cubicaltt.git / commitdiff