import helix\r
import univalence\r
\r
+-- Only ZBZ.ZEquiv is not proven\r
+-- Some proofs are replaced by undefined to speed up typechecking\r
+\r
+--\r
+\r
+lemHcomp (x : loopS1) : Id loopS1 (<i> comp (<_>S1) (x@i) [(i=0)-><_>base,(i=1)-><_>base]) x\r
+ = <j i> comp (<_>S1) (x@i) [(i=0)-><_>base,(j=1)-><_>x@i,(i=1)-><_>base]\r
+\r
+lemHcomp3 (x : loopS1)\r
+ : Id loopS1\r
+ (<i> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (x@i) [(i=0)-><_>base,(i=1)-><_>base]) [(i=0)-><_>base,(i=1)-><_>base]) [(i=0)-><_>base,(i=1)-><_>base]) x\r
+ = compId loopS1\r
+ (<i> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (x@i) [(i=0)-><_>base,(i=1)-><_>base]) [(i=0)-><_>base,(i=1)-><_>base]) [(i=0)-><_>base,(i=1)-><_>base])\r
+ (<i> comp (<_>S1) (comp (<_>S1) (x@i) [(i=0)-><_>base,(i=1)-><_>base]) [(i=0)-><_>base,(i=1)-><_>base])\r
+ x\r
+ (<j i> comp (<_>S1) (comp (<_>S1) (lemHcomp x@j@i) [(i=0)-><_>base,(i=1)-><_>base]) [(i=0)-><_>base,(i=1)-><_>base])\r
+ (compId loopS1\r
+ (<i> comp (<_>S1) (comp (<_>S1) (x@i) [(i=0)-><_>base,(i=1)-><_>base]) [(i=0)-><_>base,(i=1)-><_>base])\r
+ (<i> comp (<_>S1) (x@i) [(i=0)-><_>base,(i=1)-><_>base])\r
+ x\r
+ (<j i> comp (<_>S1) (lemHcomp x@j@i) [(i=0)-><_>base,(i=1)-><_>base])\r
+ (lemHcomp x))\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
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
+lem2ItPos : (n:nat) -> Id loopS1 (loopIt (predZ (inr n))) (backTurn (loopIt (inr n))) = split\r
+ zero -> transport (<i> Id loopS1 invLoop (lemReflComp S1 base base invLoop @ -i)) (<_> invLoop)\r
+ suc p -> compInv S1 base base (loopIt (inr p)) base loop1\r
+\r
+lem2It : (n:Z) -> Id loopS1 (loopIt (predZ n)) (backTurn (loopIt n)) = split\r
+ inl n -> <_> loopIt (inl (suc n))\r
+ inr n -> lem2ItPos n\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
s (z:T1) : Id T1 (f (g z)) z = refl T1 z\r
t (q:T0) : Id T0 (g (f q)) q = refl T0 q\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 (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
+ = 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
+-- truncation\r
+\r
hProp : U = (X : U) * prop X\r
\r
ishinh_UU (X : U) : U = (P : hProp) -> ((X -> P.1) -> P.1)\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
+-- P1 <-> P2 <-> P3\r
\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
\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
+ * ((x : A) -> isEquiv Z A (action A AShift x))\r
\r
BZSet (x : BZ) : U = x.1\r
-\r
BZASet (A : BZ) : set (BZSet A) = A.2.1\r
-\r
BZNE (A : BZ) : ishinh_UU (BZSet A) = A.2.2.1\r
-\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) = A.2.2.2.2\r
\r
+-- Two Z-torsors are equal if their underlying sets are equal in a way compatible with the actions\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
A : U = BA.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
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 (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
- = 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 : 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
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
+-- 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
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
- 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
+ -- 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 -> compId Z (predZ (plus (inr (suc (suc n))) (inl n))) (predZ (sucZ (plus (inl n) (inr (suc n))))) zeroZ\r
+ -- (<i> predZ (plusComm (inr (suc (suc n))) (inl n) @ i))\r
+ -- (compId Z (predZ (sucZ (plus (inl n) (inr (suc n))))) (predZ (sucZ (plus (inr (suc n)) (inl n)))) zeroZ\r
+ -- (<i> predZ (sucZ (plusComm (inr (suc n)) (inl n) @ -i)))\r
+ -- (<i> predZ (sucZ (hole n @ i))))\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
+ -- 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) = undefined\r
+ -- where\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
- 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
= 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 : loopBZ = (lemBZ ZBZ ZBZ).1 (sucIdZ, hole)\r
+loopA (A : BZ) : Id BZ A A = (lemBZ A A).1 (shiftId, 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
- (<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
+ AS : U = BZSet A\r
+ shiftId : Id U AS AS = equivId AS AS (BZShift A).1 (BZShift A).2\r
+ hole1 (x : AS) : Id AS (transport (<_>AS) (transport (<_> AS) (BZS A (BZS A (transport (<_> AS) (BZP A (transport (<_>AS) x))))))) (BZS A (BZS A (BZP A x)))\r
+ = compId AS (transport (<_>AS) (transport (<_> AS) (BZS A (BZS A (transport (<_> AS) (BZP A (transport (<_>AS) x)))))))\r
+ (BZS A (BZS A (transport (<_> AS) (BZP A (transport (<_>AS) x)))))\r
+ (BZS A (BZS A (BZP A x)))\r
+ (transConstNRefl AS (BZS A (BZS A (transport (<_> AS) (BZP A (transport (<_>AS) x))))) (suc (suc zero)))\r
+ (compId AS (BZS A (BZS A (transport (<_> AS) (BZP A (transport (<_>AS) x)))))\r
+ (BZS A (BZS A (BZP A (transport (<_>AS) x))))\r
+ (BZS A (BZS A (BZP A x)))\r
+ (<i> BZS A (BZS A (transRefl AS (BZP A (transport (<_>AS) x)) @ i)))\r
+ (<i> BZS A (BZS A (BZP A (transRefl AS x @ i))))\r
+ )\r
+ hole2 (x : AS) : Id AS (BZS A (BZS A (BZP A x))) (BZS A x) = <i> BZS A (retEq AS AS (BZShift A) x @ i)\r
+ hole3 : Id (AS -> AS) (transport (<i> (shiftId@i) -> (shiftId@i)) (BZS A)) (BZS A)\r
+ = <i> \(x : AS) -> compId AS (transport shiftId (BZS A (transport (<j> shiftId @ -j) x))) (BZS A (BZS A (BZP A x))) (BZS A x)\r
+ (hole1 x) (hole2 x) @ i\r
+ hole : IdP (<i> (shiftId@i) -> (shiftId@i)) (BZS A) (BZS A)\r
+ = substIdP (AS->AS) (AS->AS) (<i> (shiftId@i) -> (shiftId@i)) (BZS A) (BZS A) hole3\r
+\r
+loopZ : loopBZ = loopA ZBZ\r
+invLoopZ : loopBZ = <i> loopZ @ -i\r
+\r
+-- loopBZ = Z = loopS1\r
\r
encodeZ (A : BZ) (p : Id BZ ZBZ A) : BZSet A = transport (<i> BZSet (p@i)) zeroZ\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
+-- where\r
+-- prf : Id (equiv Z Z) (BZAction ZBZ zeroZ, BZEquiv ZBZ zeroZ) (\(x : Z) -> x, isEquivId Z) = 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
-- decodeEncodeZRefl1\r
-- : IdP (<j> (IdP (<i> decodeEncodeZRefl0@j@i -> decodeEncodeZRefl0@j@i) sucZ sucZ))\r
-- (<i> (BZShift (decodeZ ZBZ zeroZ@i)).1) (<_> sucZ)\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
+-- BZ = S1\r
+\r
+F : S1 -> BZ = split\r
+ base -> ZBZ\r
+ loop @ i -> loopZ @ i\r
+\r
+-- mapOnPath S1 BZ F base base = loopS1equalsLoopBZ'.1 : same left inverse and loopS1equalsLoopBZ'.1 is an equivalence\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
+ base -> \(x : loopBZ) -> (loopS1equalsLoopBZ'.2 x).1.1\r
loop @ i -> hole @ i\r
where\r
+ hole4 (x : Z) : Id loopS1 (loopIt (predZ x)) (compS1 (loopIt x) invLoop)\r
+ = lem2It x\r
+ hole5 (x : loopBZ) : Id Z (encodeZ ZBZ (compBZ x invLoopZ)) (predZ (encodeZ ZBZ x))\r
+ = J BZ ZBZ (\(A : BZ) -> \(x : Id BZ ZBZ A) -> Id (BZSet A) (encodeZ A (compId BZ ZBZ A A x (<i> loopA A @ -i))) (BZP A (encodeZ A x)))\r
+ (<_> inl zero) ZBZ x\r
+ hole3 (x : loopBZ)\r
+ : Id loopS1\r
+ (compS1 (decode base (encodeZ ZBZ (compBZ x invLoopZ))) loop1)\r
+ (decode base (encodeZ ZBZ x))\r
+ = compId loopS1\r
+ (compS1 (decode base (encodeZ ZBZ (compBZ x invLoopZ))) loop1)\r
+ (compS1 (decode base (predZ (encodeZ ZBZ x))) loop1)\r
+ (decode base (encodeZ ZBZ x))\r
+ (<i> compS1 (decode base (hole5 x @ i)) loop1)\r
+ (compId loopS1\r
+ (compS1 (decode base (predZ (encodeZ ZBZ x))) loop1)\r
+ (compS1 (compS1 (decode base (encodeZ ZBZ x)) invLoop) loop1)\r
+ (decode base (encodeZ ZBZ x))\r
+ (<i> compS1 (hole4 (encodeZ ZBZ x) @ i) loop1)\r
+ (<i> compInv S1 base base (decode base (encodeZ ZBZ x)) base invLoop @ -i))\r
+ hole6 (x : loopBZ) : Id loopS1 (loopS1equalsLoopBZ'.2 x).1.1 (decode base (encodeZ ZBZ x))\r
+ = compId loopS1 (loopS1equalsLoopBZ'.2 x).1.1 (loopIt (transConstN Z (encodeZ ZBZ x) (suc (suc (suc (suc (suc zero))))))) (decode base (encodeZ ZBZ x))\r
+ (lemHcomp3 (loopIt (transConstN Z (encodeZ ZBZ x) (suc (suc (suc (suc (suc zero))))))))\r
+ (<i> decode base (transConstNRefl Z (encodeZ ZBZ x) (suc (suc (suc (suc (suc zero))))) @ i))\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
+ (\(x : loopBZ) -> compS1 ((loopS1equalsLoopBZ'.2 (compBZ x invLoopZ)).1.1) loop1)\r
+ (\(x : loopBZ) -> (loopS1equalsLoopBZ'.2 x).1.1)\r
+ = <j> \(x : loopBZ) ->\r
+ transport (<i> Id loopS1 (compS1 (hole6 (compBZ x invLoopZ) @ -i) loop1) (loopS1equalsLoopBZ'.2 x).1.1)\r
+ (transport (<i> Id loopS1 (compS1 (decode base (encodeZ ZBZ (compBZ x invLoopZ))) loop1) (hole6 x @ -i))\r
+ (hole3 x)) @ j\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
+ (\(x : loopBZ) -> (loopS1equalsLoopBZ'.2 x).1.1)\r
+ (\(x : loopBZ) -> (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
+ (\(x : loopBZ) -> (loopS1equalsLoopBZ'.2 x).1.1)\r
+ (\(x : loopBZ) -> (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
+ (lemHcomp3 (<_> base))\r
\r
+-- When F_fullyFaithful.hole0 is uncommented, typechecking F_fullyFaithful.hole is slow (doesn't terminate ?)\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
(\(y : S1) -> propIsEquiv (Id S1 base y) (Id BZ ZBZ (F y)) (mapOnPath S1 BZ F base y))\r
hole)\r
where\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
+ hole0 : Id (loopS1 -> loopBZ) (mapOnPath S1 BZ F base base) loopS1equalsLoopBZ'.1\r
= undefined\r
- -- = transport (<i> isEquiv loopS1 loopBZ (hole0 @ -i)) loopS1equalsLoopBZ'.2\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
+ = 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
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
+-- Typechecking S1equalsBZ.hole is slow\r
+\r
S1equalsBZ : Id U S1 BZ = hole\r
where\r
G (y : BZ) : S1 = (F_essentiallySurjective y).1\r
projects / cubicaltt.git / commitdiff