some proofs

diff --git a/examples/torsor.ctt b/examples/torsor.ctt
index 655bb5978bbb4476c1a4ff02d5f0a5f88b27931b..f55252357ad3b1cdbfbf3d2fe7a9ed4cd33b1d00 100644 (file)
--- a/examples/torsor.ctt
+++ b/examples/torsor.ctt
@@ -10,6 +10,14 @@ import univalence
 \r
 --\r
 \r
+isEquivComp (A B C : U) (F : A -> B) (G : B -> C) (ef : isEquiv A B F) (eg : isEquiv B C G)\r
+  : isEquiv A C (\(x : A) -> G (F x))\r
+  = gradLemma A C (\(x : A) -> G (F x)) (\(x : C) -> (ef (eg x).1.1).1.1)\r
+    (\(x : C) -> compId C (G (F (ef (eg x).1.1).1.1)) (G (eg x).1.1) x\r
+                 (<i> G (retEq A B (F, ef) (eg x).1.1 @ i)) (retEq B C (G, eg) x))\r
+    (\(x : A) -> compId A ((ef (eg (G (F x))).1.1).1.1) (ef (F x)).1.1 x\r
+                 (<i> (ef (secEq B C (G, eg) (F x) @ i)).1.1) (secEq A B (F, ef) x))\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
@@ -330,6 +338,20 @@ action (A : U) (shift : equiv A A) (x : A) : Z -> A = split
       zero  -> x\r
       suc n -> shift.1 (action A shift x (inr n))\r
 \r
+actionEquiv (A : U) (shift : equiv A A) : (y : Z) -> isEquiv A A (\(x : A) -> action A shift x y) = split\r
+  inl n -> hole n\r
+    where hole : (n : nat) -> isEquiv A A (\(x : A) -> action A shift x (inl n)) = split\r
+      zero -> hole0\r
+        where hole0 : isEquiv A A (\(x : A) -> action A shift x (inl zero)) = undefined\r
+      suc n -> hole0\r
+        where hole0 : isEquiv A A (\(x : A) -> (shift.2 (action A shift x (inl n))).1.1) = undefined\r
+  inr n -> hole n\r
+    where hole : (n : nat) -> isEquiv A A (\(x : A) -> action A shift x (inr n)) = split\r
+      zero -> isEquivId A\r
+      suc n -> isEquivComp A A A (\(x : A) -> action A shift x (inr n)) shift.1 (hole n) shift.2\r
+\r
+plop : nat = U\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
@@ -575,11 +597,8 @@ decodeZ (A : BZ) (a : BZSet A) : Id BZ ZBZ A = (lemBZ ZBZ A).1 (<i> p @ -i, <i>
       = 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
---     where\r
---       prf : Id (equiv Z Z) (BZAction ZBZ zeroZ, BZEquiv ZBZ zeroZ) (\(x : Z) -> x, isEquivId Z) = hole\r
+prf : Id (equiv Z Z) (BZAction ZBZ zeroZ, BZEquiv ZBZ zeroZ) (\(x : Z) -> x, isEquivId Z) = undefined\r
+-- hole\r
 --         where\r
 --           hole0 : (x : Z) -> Id Z (BZAction ZBZ zeroZ x) x = split\r
 --             inl n -> hole1 n\r
@@ -600,119 +619,124 @@ decodeZ (A : BZ) (a : BZSet A) : Id BZ ZBZ A = (lemBZ ZBZ A).1 (<i> p @ -i, <i>
 --                    (<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
---   = 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
+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
 \r
-loopBZequalsZ : Id U loopBZ Z = isoId loopBZ Z (encodeZ ZBZ) (decodeZ ZBZ) (encodeDecodeZ ZBZ) (decodeEncodeZ ZBZ)\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
 \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
+-- 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
-F : S1 -> BZ = split\r
-  base -> ZBZ\r
-  loop @ i -> loopZ @ i\r
+-- decodeEncodeZ : (A : BZ) -> (p : Id BZ ZBZ A) -> Id (Id BZ ZBZ A) (decodeZ A (encodeZ A p)) p\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
+--   = lem0 Z (BZSet A) (BZAction A p) (BZEquiv A p) zeroZ\r
 \r
--- mapOnPath S1 BZ F base base = loopS1equalsLoopBZ'.1 : same left inverse and loopS1equalsLoopBZ'.1 is an equivalence\r
+-- loopBZequalsZ : Id U loopBZ Z = isoId loopBZ Z (encodeZ ZBZ) (decodeZ ZBZ) (encodeDecodeZ ZBZ) (decodeEncodeZ ZBZ)\r
 \r
-G : (y : S1) -> Id BZ ZBZ (F y) -> Id S1 base y = split\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 : 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 : 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 : 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
-     (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
-               (\(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
-    hole0 : Id (loopS1 -> loopBZ) (mapOnPath S1 BZ F base base) loopS1equalsLoopBZ'.1\r
-         = undefined\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
+-- 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
-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)) = 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
+-- -- BZ = S1\r
 \r
--- Typechecking S1equalsBZ.hole is slow\r
+-- F : S1 -> BZ = split\r
+--   base -> ZBZ\r
+--   loop @ i -> loopZ @ i\r
 \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
+-- -- 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 : 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 : 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 : 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 : 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
+--      (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
+--                (\(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
+--     hole0 : Id (loopS1 -> loopBZ) (mapOnPath S1 BZ F base base) loopS1equalsLoopBZ'.1\r
+--          = undefined\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
+--     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
+-- -- 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
+--     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