The loop space of the torus is equal to Z * Z

diff --git a/examples/mystery.ctt b/examples/mystery.ctt
index a93d68ad653807391827bcaf5ea96317c5f18266..db63cbeaab8590a73fbb4be87eafdce30b667e43 100644 (file)
--- a/examples/mystery.ctt
+++ b/examples/mystery.ctt
@@ -11,8 +11,6 @@ import torus
 -- (5) convert back to (loopS1 * loopS1)
 -- (6) convert back to (Z * Z)
 
-loopT : U = IdP (<_>Torus) ptT ptT
-
 -- use transport to lift just because we can :)
 Zs_to_loopS1s (input : and (and Z Z) (and Z Z)) : and (and loopS1 loopS1) (and loopS1 loopS1) =
    transport (<i> and (and (loopS1equalsZ @ -i) (loopS1equalsZ @ -i)) (and (loopS1equalsZ @ -i) (loopS1equalsZ @ -i))) input

diff --git a/examples/sigma.ctt b/examples/sigma.ctt
index a442e9b7b5431b28de933cc4fdc697d440192a10..7b3d7a25a2ee351266bebbd37909b23bf272044a 100644 (file)
--- a/examples/sigma.ctt
+++ b/examples/sigma.ctt
@@ -5,16 +5,20 @@ import equiv
 
 -- application of this fact
 
-sig (A:U) (P : A -> U) : U = (x:A) * P x
-
-lemIdSig  (A:U) (B:A-> U) (t u : sig A B) : Id U (Id (sig A B) t u) ((p:Id A t.1 u.1) * IdP (<i> B (p@i)) t.2 u.2) =
- isoId T0 T1 f g s t where
-  T0 : U = Id (sig A B) t u
-  T1 : U = (p:Id A t.1 u.1) * IdP (<i> B (p@i)) t.2 u.2
-  f (q:T0) : T1 = (<i> (q@i).1,<i> (q@i).2)
-  g (z:T1) : T0 = <i>(z.1 @i,z.2 @i)
-  s (z:T1) : Id T1 (f (g z)) z = refl T1 z
-  t (q:T0) : Id T0 (g (f q)) q = refl T0 q
+sig (A : U) (P : A -> U) : U = (x : A) * P x
+
+lemIdSig (A:U) (B : A -> U) (t u : sig A B) :
+ Id U (Id (sig A B) t u) ((p : Id A t.1 u.1) * IdP (<i> B (p @ i)) t.2 u.2) =
+  isoId T0 T1 f g s t where
+   T0 : U = Id (sig A B) t u
+   T1 : U = (p:Id A t.1 u.1) * IdP (<i> B (p@i)) t.2 u.2
+   f (q:T0) : T1 = (<i> (q@i).1,<i> (q@i).2)
+   g (z:T1) : T0 = <i>(z.1 @i,z.2 @i)
+   s (z:T1) : Id T1 (f (g z)) z = refl T1 z
+   t (q:T0) : Id T0 (g (f q)) q = refl T0 q
+
+lemIdAnd (A B : U) (t u : and A B) :
+  Id U (Id (and A B) t u) (and (Id A t.1 u.1) (Id B t.2 u.2)) = lemIdSig A (\(_ : A) -> B) t u
 
 lem (A:U) (P:A->U) (pP:(x:A) -> prop (P x)) (u v:(x:A) * P x) (p:Id A u.1 v.1) :
  Id ((x:A)*P x) u v = <i>(p@i,(lemPropF A P pP u.1 v.1 p u.2 v.2)@i)

diff --git a/examples/torus.ctt b/examples/torus.ctt
index 256d85d0be2f8c0270440e750b82275232e66252..84d4c29fdcea85437f9315ea53877ec243b16a71 100644 (file)
--- a/examples/torus.ctt
+++ b/examples/torus.ctt
@@ -1,6 +1,7 @@
 module torus where
 
-import circle
+import sigma
+import helix
 
 data Torus = ptT
            | pathOneT <i> [ (i=0) -> ptT, (i=1) -> ptT ]
@@ -174,3 +175,16 @@ diag_of_image_of_ff : IdP (<_> (_ : S1) * S1) (base,base) (base,base)
 S1S1equalsTorus : Id U (and S1 S1) Torus = isoId (and S1 S1) Torus c2t t2c t2c2t rem
  where
  rem (c:and S1 S1) : Id (and S1 S1) (t2c (c2t c)) c = c2t2c c.1 c.2
+
+TorusEqualsS1S1 : Id U Torus (and S1 S1) = <i> S1S1equalsTorus @ -i
+
+loopT : U = Id Torus ptT ptT
+
+loopTorusEqualsZZ : Id U loopT (and Z Z) = <i> comp U (rem @ i) [(i = 1) -> rem1]
+  where
+  rem : Id U loopT (Id (and S1 S1) (base,base) (base,base)) =
+    funDep Torus (and S1 S1) TorusEqualsS1S1 ptT (base,base)
+
+  rem1 : Id U (Id (and S1 S1) (base,base) (base,base)) (and Z Z) =
+    <i> comp U (lemIdAnd S1 S1 (base,base) (base,base) @ i)
+             [(i = 1) -> <j> and (loopS1equalsZ @ j) (loopS1equalsZ @ j)]