.

diff --git a/examples/torsor.ctt b/examples/torsor.ctt
new file mode 100644 (file)
index 0000000..0fc4d7b
--- /dev/null
+++ b/examples/torsor.ctt
@@ -0,0 +1,297 @@
+module torsor where\r
+import circle\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
+  isoId T0 T1 f g s t where\r
+   T0 : U = Id (Sigma A B) t u\r
+   T1 : U = (p:Id A t.1 u.1) * IdP (<i> B (p@i)) t.2 u.2\r
+   f (q:T0) : T1 = (<i> (q@i).1,<i> (q@i).2)\r
+   g (z:T1) : T0 = <i>(z.1 @i,z.2 @i)\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
+hProp : U = (X : U) * prop X\r
+\r
+ishinh_UU (X : U) : U = (P : hProp) -> ((X -> P.1) -> P.1)\r
+\r
+propishinh (X : U) : prop (ishinh_UU X) =\r
+  propPi hProp (\(P : hProp) -> ((X -> P.1) -> P.1)) rem1\r
+  where\r
+   rem1 (P : hProp) : prop ((X -> P.1) -> P.1) =\r
+     propPi (X -> P.1) (\(_ : X -> P.1) -> P.1) (\(f : X -> P.1) -> P.2)\r
+\r
+ishinh (X : U) : hProp = (ishinh_UU X,propishinh X)\r
+\r
+hinhpr (X : U) : X -> (ishinh X).1 =\r
+  \(x : X) (P : hProp) (f : X -> P.1) -> f x\r
+\r
+--\r
+\r
+-- A : U = undefined\r
+-- B : U = undefined\r
+-- F : A -> B = undefined\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
+\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
+\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
+\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
+\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
+-- 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
+-- 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
+-- 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
+\r
+transRefl (A : U) (a : A) : Id A (transport (<_> A) a) a = <i> comp (<_> A) a [(i=1) -> <_>a]\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
+\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
+\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
+\r
+BZSet : BZ -> U = split\r
+  bz A ASet a AShift AEquiv -> A\r
+\r
+BZASet : (A : BZ) -> set (BZSet A) = split\r
+  bz A ASet a AShift AEquiv -> ASet\r
+\r
+BZNE : (A : BZ) -> ishinh_UU (BZSet A) = split\r
+  bz A ASet a AShift AEquiv -> a\r
+\r
+BZShift : (A : BZ) -> equiv (BZSet A) (BZSet A) = split\r
+  bz A ASet a AShift AEquiv -> AShift\r
+\r
+BZS (A : BZ) : BZSet A -> BZSet A = (BZShift A).1\r
+\r
+BZEquiv : (A : BZ) -> (x : BZSet A) -> isEquiv Z (BZSet A) (action (BZSet A) (BZShift 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
+  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
+        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
+              where\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
+\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
+\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
+\r
+loopZ : Id BZ ZBZ ZBZ = lemBZ ZBZ ZBZ sucIdZ q\r
+  where\r
+    q : IdP (<i> (sucIdZ@i) -> (sucIdZ@i)) sucZ sucZ = undefined\r
+    hole : U = U\r
+\r
+F : S1 -> BZ = split\r
+  base -> ZBZ\r
+  loop @ i -> loopZ @ i\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
+    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
+\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
+    hole   : (x : S1) * Id BZ y (F x) = hContr.1\r