slow proof

diff --git a/examples/torsor0.ctt b/examples/torsor0.ctt
new file mode 100644 (file)
index 0000000..0825628
--- /dev/null
+++ b/examples/torsor0.ctt
@@ -0,0 +1,258 @@
+module torsor0 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
+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
+    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
+       : Id (Id ((x : A) -> B x) f0 f1) p1 p2\r
+  = <i j> \(x : A) -> (h x (f0 x) (f1 x) (<i> (p1@i) x) (<i> (p2@i) x)) @ i @ j\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
+lemIdPSet (A B : U) (ASet : set A) (p : Id U A B) : (x : A) (y : B) (s t : IdP p x y) -> Id (IdP p x y) s t\r
+  = J U A (\(B : U) -> \(p : Id U A B) -> (x : A) (y : B) (s t : IdP p x y) -> Id (IdP p x y) s t) ASet B p\r
+\r
+lemIdPSet2 (A B : U) (ASet : set A) (p1 : Id U A B)\r
+  : (p2 : Id U A B) -> (p : Id (Id U A B) p1 p2) ->\r
+    (x : A) -> (y : B) -> (s : IdP p1 x y) -> (t : IdP p2 x y) -> IdP (<i> (IdP (p @ i) x y)) s t\r
+  = J (Id U A B) p1 (\(p2 : Id U A B) -> \(p : Id (Id U A B) p1 p2) -> (x : A) -> (y : B) -> (s : IdP p1 x y) -> (t : IdP p2 x y) -> IdP (<i> (IdP (p @ i) x y)) s t)\r
+    (lemIdPSet A B ASet p1)\r
+\r
+\r
+isEquivId (A : U) : isEquiv A A (\(x : A) -> x) = gradLemma A A (\(x : A) -> x) (\(x : A) -> x) (\(x : A) -> <_> x) (\(x : A) -> <_> x)\r
+\r
+lem10 (A B : U) (e : equiv A B) (x y : B) (p : Id A (e.2 x).1.1 (e.2 y).1.1) : Id B x y\r
+  = transport\r
+    (compId U (Id B (e.1 (e.2 x).1.1) (e.1 (e.2 y).1.1)) (Id B x (e.1 (e.2 y).1.1)) (Id B x y)\r
+     (<i> Id B (retEq A B e x @ i) (e.1 (e.2 y).1.1)) (<i> Id B x (retEq A B e y @ i)))\r
+    (mapOnPath A B e.1 (e.2 x).1.1 (e.2 y).1.1 p)\r
+\r
+lem10' (A B : U) (e : equiv A B) (x y : A) (p : Id B (e.1 x) (e.1 y)) : Id A x y\r
+  = transport\r
+    (compId U (Id A (e.2 (e.1 x)).1.1 (e.2 (e.1 y)).1.1) (Id A x (e.2 (e.1 y)).1.1) (Id A x y)\r
+     (<i> Id A (secEq A B e x @ i) (e.2 (e.1 y)).1.1) (<i> Id A x (secEq A B e y @ i))\r
+     )\r
+    (mapOnPath B A (invEq A B e) (e.1 x) (e.1 y) p)\r
+\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
+               (\(x : A) -> x, isEquivId A)\r
+               (transEquiv' A A (<_> A))\r
+                 = <i> ( (transRefl (A->A) (\(x : A) -> x) @ -i)\r
+                       , lemIdPProp (isEquiv A A (\(x : A) -> x)) (isEquiv A A (transEquiv' A A (<_> A)).1)\r
+                         (propIsEquiv A A (\(x : A) -> x)) (<j> isEquiv A A (transRefl (A->A) (\(x : A) -> x) @ -j))\r
+                         (isEquivId A) (transEquiv' A A (<_> A)).2 @ i\r
+                       )\r
+    hole1 : Id (equiv A A) (transEquiv' A A (univalence A A (\(x : A) -> x, isEquivId A)).1.1) (\(x : A) -> x, isEquivId A)\r
+      = retEq (Id U A A) (equiv A A) (corrUniv' A A) (\(x : A) -> x, isEquivId A)\r
+    hole : Id (Id U A A) (univalence A A (\(x : A) -> x, isEquivId A)).1.1 (<_> A)\r
+      = lem10' (Id U A A) (equiv A A) (corrUniv' A A)\r
+        (univalence A A (\(x : A) -> x, isEquivId A)).1.1 (<_> A)\r
+        (compId (equiv A A) (transEquiv' A A (univalence A A (\(x : A) -> x, isEquivId A)).1.1) (\(x : A) -> x, isEquivId A) (transEquiv' A A (<_> A)) hole1 hole0)\r
+\r
+substIdP (A B : U) (p : Id U A B) (x : A) (y : B) (q : Id B (transport p x) y) : IdP p x y\r
+  = transport (<i> IdP p x (q@i)) hole\r
+  where\r
+    hole : IdP p x (transport p x) = <i> comp (<j> p @ (i /\ j)) x [(i=0) -> <_> x]\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
+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
+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
+inhPropContr (A : U) (x : prop A) (y : ishinh_UU A) : isContr A = y (isContr A, propIsContr A) (\(z : A) -> (z, x z))\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
+\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 (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
+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
+\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
+      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
+      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 = undefined\r
+          pNE   : IdP (<i> ishinh_UU (p@i)) a b = undefined\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 = undefined\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 = undefined\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
+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 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 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 = (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
+    ZEquiv (x : Z) : 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
+-- loopBZ = Z = loopS1\r
+\r
+encodeZ (A : BZ) (p : Id BZ ZBZ A) : BZSet A = transport (<i> BZSet (p@i)) zeroZ\r
+\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
+    q : IdP (<i> (p@i) -> (p@i)) (BZS A) sucZ = undefined\r
+\r
+prf : Id (equiv Z Z) (BZAction ZBZ zeroZ, BZEquiv ZBZ zeroZ) (\(x : Z) -> x, isEquivId Z) = undefined\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
+\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
+\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