torsor multiplication

diff --git a/examples/torsor.ctt b/examples/torsor.ctt
index 3581c3723befe7cc65c3747407c80dca1dc542da..2f2ad37917e12ec136faa4461eb404a1411510fb 100644 (file)
--- a/examples/torsor.ctt
+++ b/examples/torsor.ctt
@@ -360,38 +360,35 @@ actionEquiv (A : U) (shift : equiv A A) : (y : Z) -> isEquiv A A (\(x : A) -> ac
       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
-BZ : U = (A : U) * (ASet : set A) * (a : ishinh_UU A)\r
+BZ : U = (A : U) * (a : ishinh_UU A)\r
        * (AShift : equiv A A)\r
        * ((x : A) -> isEquiv Z A (action A AShift x))\r
 \r
 BZSet (x : BZ) : U = x.1\r
-BZASet (A : BZ) : set (BZSet A) = A.2.1\r
-BZNE (A : BZ) : ishinh_UU (BZSet A) = A.2.2.1\r
-BZShift (A : BZ) : equiv (BZSet A) (BZSet A) = A.2.2.2.1\r
+BZNE (A : BZ) : ishinh_UU (BZSet A) = A.2.1\r
+BZShift (A : BZ) : equiv (BZSet A) (BZSet A) = A.2.2.1\r
 BZAction (A : BZ) : BZSet A -> Z -> BZSet A = action (BZSet A) (BZShift A)\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
-BZEquiv (A : BZ) : (x : BZSet A) -> isEquiv Z (BZSet A) (BZAction A x) = A.2.2.2.2\r
+BZEquiv (A : BZ) : (x : BZSet A) -> isEquiv Z (BZSet A) (BZAction A x) = A.2.2.2\r
+BZASet (x : BZ) : set (BZSet x) = BZNE x (set (BZSet x), setIsProp (BZSet x))\r
+                                  (\(a : BZSet x) -> transport (<i> set (equivId Z (BZSet x) (BZAction x a) (BZEquiv x a) @ i)) ZSet)\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
-      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
+      a : ishinh_UU A = BA.2.1\r
+      AShift : equiv A A = BA.2.2.1\r
+      AEquiv : (x : A) -> isEquiv Z A (BZAction BA x) = BA.2.2.2\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
+      b : ishinh_UU B = BB.2.1\r
+      BShift : equiv B B = BB.2.2.1\r
+      BEquiv : (x : B) -> isEquiv Z B (BZAction BB x) = BB.2.2.2\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
@@ -411,7 +408,7 @@ lemBZ (BA BB : BZ) : equiv ((p : Id U (BZSet BA) (BZSet BB)) * IdP (<i> p@i -> p
                     (\(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
+          hole : Id BZ BA BB = <i> (p@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
@@ -421,8 +418,6 @@ lemBZ (BA BB : BZ) : equiv ((p : Id U (BZSet BA) (BZSet BB)) * IdP (<i> p@i -> p
           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
@@ -446,7 +441,7 @@ lemBZ (BA BB : BZ) : equiv ((p : Id U (BZSet BA) (BZSet BB)) * IdP (<i> p@i -> p
                    (<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 : Id (Id BZ BA BB) q2 q = <j i> (p@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
@@ -474,7 +469,7 @@ lem2' (A : U) (shift : equiv A A) (a : A) : (x : Z) -> Id A (shift.2 (action A s
         zero  -> <_> action A shift a (inl zero)\r
         suc n -> secEq A A shift (action A shift a (inr n))\r
 \r
-ZBZ : BZ = (Z, (ZSet, (hinhpr Z zeroZ, (ZShift, ZEquiv))))\r
+ZBZ : BZ = (Z, (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
@@ -598,6 +593,7 @@ decodeZQ (A : BZ) (a : BZSet A) : IdP (<i> ((decodeZP A a)@-i) -> ((decodeZP A a
          = <i> substIdP (BZSet A -> BZSet A) (Z -> Z) (<i> ((decodeZP A a)@i) -> ((decodeZP A a)@i)) (BZS A) sucZ (decodeZ3 A a) @ -i\r
 opaque decodeZQ\r
 \r
+decodeZ (A : BZ) (a : BZSet A) : Id BZ ZBZ A = (lemBZ ZBZ A).1 (<i> decodeZP A a @ -i, decodeZQ A a)\r
 \r
 AA : U = (X : U) * (X -> X)\r
 BZ' : U = (X : AA) * ishinh_UU (Id AA X (Z, sucZ))\r
@@ -606,9 +602,8 @@ BZequivBZ' : Id U BZ BZ' = isoId BZ BZ' F G FG GF
     F (A : BZ) : BZ' = ((BZSet A, BZS A), BZNE A (ishinh (Id AA (BZSet A, BZS A) (Z, sucZ)))\r
                         (\(a : BZSet A) -> hinhpr (Id AA (BZSet A, BZS A) (Z, sucZ)) (<i> (decodeZP A a @ i, decodeZQ A a @ -i))))\r
     G (A : BZ') : BZ = (A.1.1,\r
-                       (A.2 (set A.1.1, setIsProp A.1.1) (\(a : Id AA A.1 (Z, sucZ)) -> transport (<i> set (a @ -i).1) ZSet),\r
                        (A.2 (ishinh A.1.1) (\(a : Id AA A.1 (Z, sucZ)) -> hinhpr A.1.1 (transport (<i> (a @ -i).1) zeroZ)),\r
-                       ((A.1.2, SHIFT), EQUIV))))\r
+                       ((A.1.2, SHIFT), EQUIV)))\r
                        where\r
                          SHIFT : isEquiv A.1.1 A.1.1 A.1.2\r
                                = A.2 (isEquiv A.1.1 A.1.1 A.1.2, propIsEquiv A.1.1 A.1.1 A.1.2)\r
@@ -630,8 +625,6 @@ BZequivBZ' : Id U BZ BZ' = isoId BZ BZ' F G FG GF
     FG (A : BZ') : Id BZ' (F (G A)) A = <i> ((A.1.1, A.1.2), propishinh (Id AA (A.1.1, A.1.2) (Z, sucZ)) (F (G A)).2 A.2 @ i)\r
     GF (A : BZ) : Id BZ (G (F A)) A = (lemBZ (G (F A)) A).1 (<_> BZSet A, <_> BZS A)\r
 \r
-decodeZ (A : BZ) (a : BZSet A) : Id BZ ZBZ A = (lemBZ ZBZ A).1 (<i> decodeZP A a @ -i, decodeZQ A a)\r
-\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
@@ -687,6 +680,75 @@ encodeDecodeZ (A : BZ) (p : BZSet A) : Id (BZSet A) (transport (univalence (BZSe
   = lem0 Z (BZSet A) (BZAction A p) (BZEquiv A p) zeroZ\r
 opaque encodeDecodeZ\r
 \r
+encodeLoop (x : loopBZ) : Id Z (encodeZ ZBZ (compBZ x loopZ)) (sucZ (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 (loopA A))) (BZS A (encodeZ A x)))\r
+     (<_> inr (suc zero)) ZBZ x\r
+opaque encodeLoop\r
+\r
+encodeInvLoop (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
+opaque encodeInvLoop\r
+\r
+decodeLoop (z : Z) : Id loopBZ (compBZ (decodeZ ZBZ z) loopZ) (decodeZ ZBZ (sucZ z))\r
+  = transport (<i> Id loopBZ (decodeEncodeZ ZBZ (compBZ (decodeZ ZBZ z) loopZ) @ i) (decodeZ ZBZ (sucZ (encodeDecodeZ ZBZ z @ i))))\r
+    (<i> decodeZ ZBZ (encodeLoop (decodeZ ZBZ z) @ i))\r
+opaque decodeLoop\r
+decodeInvLoop (z : Z) : Id (Id BZ ZBZ ZBZ) (compBZ (decodeZ ZBZ z) invLoopZ) (decodeZ ZBZ (predZ z))\r
+  = transport (<i> Id loopBZ (decodeEncodeZ ZBZ (compBZ (decodeZ ZBZ z) invLoopZ) @ i) (decodeZ ZBZ (predZ (encodeDecodeZ ZBZ z @ i))))\r
+    (<i> decodeZ ZBZ (encodeInvLoop (decodeZ ZBZ z) @ i))\r
+opaque decodeInvLoop\r
+\r
+multZ (A B : BZ) : BZ = (T, (TNE, (TShift A B, TEquiv)))\r
+  where\r
+    opaque decodeZ\r
+    opaque loopA\r
+    T      : U = Id BZ A B\r
+    TNE    : ishinh_UU T = BZNE A (ishinh T) (\(a : BZSet A) -> BZNE B (ishinh T) (\(b : BZSet B) ->\r
+                            hinhpr T (compId BZ A ZBZ B (<i> decodeZ A a @ -i) (decodeZ B b))))\r
+    F (A B : BZ) (x : (Id BZ A B)) : (Id BZ A B) = compId BZ A B B x (loopA B)\r
+    G (A B : BZ) (x : (Id BZ A B)) : (Id BZ A B) = compId BZ A B B x (<i> loopA B @ -i)\r
+    FG (A B : BZ) (x : (Id BZ A B)) : Id (Id BZ A B) (F A B (G A B x)) x = lemCompInv BZ A B B x (<i> loopA B @ -i)\r
+    opaque FG\r
+    GF (A B : BZ) (x : (Id BZ A B)) : Id (Id BZ A B) (G A B (F A B x)) x = lemCompInv BZ A B B x (loopA B)\r
+    opaque GF\r
+    TShift (A B : BZ) : equiv (Id BZ A B) (Id BZ A B) = (F A B, gradLemma (Id BZ A B) (Id BZ A B) (F A B) (G A B) (FG A B) (GF A B))\r
+    hole : (y : Z) -> Id (Id BZ ZBZ ZBZ) (action (Id BZ ZBZ ZBZ) (TShift ZBZ ZBZ) (<_> ZBZ) y) (decodeZ ZBZ y) = split\r
+      inl u -> hole0 u\r
+        where hole0 : (n : nat) -> Id (Id BZ ZBZ ZBZ) (action (Id BZ ZBZ ZBZ) (TShift ZBZ ZBZ) (<_> ZBZ) (inl n)) (decodeZ ZBZ (inl n)) = split\r
+          zero -> hole1\r
+            where hole1 : Id (Id BZ ZBZ ZBZ) (compBZ (<_> ZBZ) invLoopZ) (decodeZ ZBZ (inl zero))\r
+                        = compId loopBZ (compBZ (<_> ZBZ) invLoopZ) (compBZ (decodeZ ZBZ (inr zero)) invLoopZ) (decodeZ ZBZ (inl zero))\r
+                          (<i> compBZ (decodeEncodeZRefl @ -i) invLoopZ)\r
+                          (decodeInvLoop (inr zero))\r
+          suc n -> hole1\r
+            where hole1 : Id (Id BZ ZBZ ZBZ) (compBZ (action loopBZ (TShift ZBZ ZBZ) (<_> ZBZ) (inl n)) invLoopZ) (decodeZ ZBZ (inl (suc n)))\r
+                        = compId (Id BZ ZBZ ZBZ) (compBZ (action (Id BZ ZBZ ZBZ) (TShift ZBZ ZBZ) (<_> ZBZ) (inl n)) invLoopZ)\r
+                          (compBZ (decodeZ ZBZ (inl n)) invLoopZ) (decodeZ ZBZ (inl (suc n)))\r
+                          (<i> compBZ (hole0 n @ i) invLoopZ)\r
+                          (decodeInvLoop (inl n))\r
+      inr u -> hole0 u\r
+        where hole0 : (n : nat) -> Id (Id BZ ZBZ ZBZ) (action (Id BZ ZBZ ZBZ) (TShift ZBZ ZBZ) (<_> ZBZ) (inr n)) (decodeZ ZBZ (inr n)) = split\r
+          zero -> <i> decodeEncodeZRefl @ -i\r
+          suc n -> compId (Id BZ ZBZ ZBZ) (compBZ (action (Id BZ ZBZ ZBZ) (TShift ZBZ ZBZ) (<_> ZBZ) (inr n)) loopZ)\r
+                          (compBZ (decodeZ ZBZ (inr n)) loopZ) (decodeZ ZBZ (inr (suc n)))\r
+                          (<i> compBZ (hole0 n @ i) loopZ)\r
+                          (decodeLoop (inr n))\r
+    visible decodeZ\r
+    TEquiv''' : isEquiv Z (Id BZ ZBZ ZBZ) (action (Id BZ ZBZ ZBZ) (TShift ZBZ ZBZ) (<_> ZBZ))\r
+      = transport (<i> isEquiv Z loopBZ (\(y : Z) -> hole y @ -i)) (gradLemma Z loopBZ (decodeZ ZBZ) (encodeZ ZBZ) (decodeEncodeZ ZBZ) (encodeDecodeZ ZBZ))\r
+    TEquiv'' (b : BZSet B) (x : Id BZ ZBZ B) : isEquiv Z (Id BZ ZBZ B) (action (Id BZ ZBZ B) (TShift ZBZ B) x)\r
+      = J BZ ZBZ (\(B : BZ) -> \(x : Id BZ ZBZ B) -> isEquiv Z (Id BZ ZBZ B) (action (Id BZ ZBZ B) (TShift ZBZ B) x))\r
+        TEquiv''' B x\r
+    TEquiv' (a : BZSet A) (b : BZSet B) : (x : T) -> isEquiv Z T (action T (TShift A B) x)\r
+       = J BZ ZBZ (\(A : BZ) -> \(p : Id BZ ZBZ A) -> (x : Id BZ A B) -> isEquiv Z (Id BZ A B) (action (Id BZ A B) (TShift A B) x))\r
+         (TEquiv'' b) A (decodeZ A a)\r
+    TEquiv (x : T) : isEquiv Z T (action T (TShift A B) x)\r
+       = BZNE A (isEquiv Z T (action T (TShift A B) x), propIsEquiv Z T (action T (TShift A B) x))\r
+         (\(a : BZSet A) -> BZNE B (isEquiv Z T (action T (TShift A B) x), propIsEquiv Z T (action T (TShift A B) x))\r
+         (\(b : BZSet B) -> TEquiv' a b x))\r
+visible decodeZ\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
@@ -706,9 +768,6 @@ G : (y : S1) -> Id BZ ZBZ (F y) -> Id S1 base y = split
     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
@@ -717,7 +776,7 @@ G : (y : S1) -> Id BZ ZBZ (F y) -> Id S1 base y = split
                 (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
+                (<i> compS1 (decode base (encodeInvLoop 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
@@ -791,4 +850,6 @@ doubleLoopBZ : loopBZ -> loopBZ = transport (<i> loopS1equalsLoopBZ@i -> loopS1e
 -- EVAL: inr (suc (suc zero))\r
 -- Time: 0m25.191s\r
 \r
--- visible_all\r
+-- > let visible_all in let doubleLoop : Id BZ (multZ ZBZ ZBZ) (multZ ZBZ ZBZ) = <i> multZ (loopZ@-i) (loopZ@i) in transport (<j> BZSet (transport (<i> BZSet (doubleLoop @ i)) (<_> ZBZ) @ j)) zeroZ\r
+\r
+visible_all\r