Patch and clean the torus example

diff --git a/examples/circle.ctt b/examples/circle.ctt
index 126b3192cbcdc567afc649e362b9bbdd6e0f7595..59c608a882952f98316da451fe444ce4db341c47 100644 (file)
--- a/examples/circle.ctt
+++ b/examples/circle.ctt
@@ -64,3 +64,10 @@ triv : loopS1 = <i> base
 -- around the circle and then back is contractible:
 hmtpy : Id loopS1 (<i> base) (<i> loop{S1} @ (i /\ -i)) =
   <j i> loop{S1} @ j /\ i /\ -i
+
+
+-- the loop space of the circle is equal to Z
+
+-- loopS1equalsZ : Id U loopS1 Z = undefined
+--  isoId loopS1 Z (encode base) (decode base) decodeEncodeBase (encodeDecode base)
+

diff --git a/examples/torus.ctt b/examples/torus.ctt
new file mode 100644 (file)
index 0000000..871e23f
--- /dev/null
+++ b/examples/torus.ctt
@@ -0,0 +1,147 @@
+-- Proof that Torus = S1 * S1 by Dan Licata.
+module torus where
+
+import sigma
+import circle
+
+data Torus = ptT
+           | pathOneT <i> [ (i=0) -> ptT, (i=1) -> ptT ]
+           | pathTwoT <i> [ (i=0) -> ptT, (i=1) -> ptT ]
+           | squareT <i j> [ (i=0) -> pathOneT {Torus} @ j
+                           , (i=1) -> pathOneT {Torus} @ j
+                           , (j=0) -> pathTwoT {Torus} @ i
+                           , (j=1) -> pathTwoT {Torus} @ i ]
+
+-- Torus = S1 * S1 proof
+
+--                  pathTwoT x
+--              ________________
+--              |              |
+--   pathOneT y | squareT x y  | pathOneT y
+--              |              |
+--              |              |
+--              ________________
+--                  pathTwoT x
+
+-- pathOneT is (loop,refl)
+-- pathTwoT is (refl,loop)
+
+-- ----------------------------------------------------------------------
+-- function from the torus to two circles
+
+t2c : Torus -> and S1 S1 = split
+  ptT -> (base,base)
+  pathOneT @ y -> (loop1 @ y, base)
+  pathTwoT @ x -> (base, loop1 @ x)
+  squareT @ x y -> (loop1 @ y, loop1 @ x)
+
+-- ----------------------------------------------------------------------
+-- function from two circles to the torus
+
+-- branch for base
+c2t_base : S1 -> Torus = split 
+  base -> ptT
+  loop @ x -> pathTwoT{Torus} @ x
+
+-- branch for loop
+c2t_loop' : (c : S1) -> IdP (<_>Torus) (c2t_base c) (c2t_base c) = split
+   base -> < x > pathOneT{Torus} @ x
+   loop @ y -> < x > squareT{Torus} @ y @ x
+
+-- use funext to exchange the interval variable and the S1 variable
+c2t_loop : IdP (<_>S1 -> Torus) c2t_base c2t_base =
+   <y> \(c : S1) -> c2t_loop' c @ y
+
+c2t' : S1 -> S1 -> Torus = split
+  base -> c2t_base 
+  loop @ y -> c2t_loop @ y
+
+c2t (cs : and S1 S1) : Torus = c2t' cs.1 cs.2
+
+------------------------------------------------------------------------
+-- first composite: induct and reflexivity! 
+
+t2c2t : (t : Torus) -> IdP (<_> Torus) (c2t (t2c t)) t = split 
+  ptT -> <_> ptT
+  pathOneT @ y -> <_> pathOneT{Torus} @ y
+  pathTwoT @ x -> <_> pathTwoT{Torus} @ x
+  squareT @ x y -> <_> squareT{Torus} @ x @ y
+
+------------------------------------------------------------------------
+-- second composite: induct and reflexivity!
+-- except we need to use the same tricks as in c2t to do the inner
+-- induction
+
+c2t2c_base : (c2 : S1) -> IdP (<_> and S1 S1) (t2c (c2t_base c2)) (base,c2) = split
+  base -> <_> (base,base)
+  loop @ y -> <_> (base,loop1 @ y)
+
+-- the loop goal reduced using the defintional equalties, and with the two binders exchanged.
+-- c2t' (loop @ y) c2 = (c2t_loop @ y c2) = c2t_loop' c2 @ y
+c2t2c_loop' : (c2 : S1) ->
+      IdP (<y> IdP (<_> and S1 S1) (t2c (c2t_loop @ y c2)) (loop1 @ y , c2))
+          (c2t2c_base c2)
+          (c2t2c_base c2) = split 
+    base -> <y> <_> (loop1 @ y, base)
+    loop @ x -> <y> <_> (loop1 @ y, loop1 @ x)
+
+c2t2c : (c1 : S1) (c2 : S1) -> IdP (<_> and S1 S1) (t2c (c2t' c1 c2)) (c1,c2) = split
+     base -> c2t2c_base
+                 -- again, I shouldn't need to do funext here;
+                 -- I should be able to do a split inside of an interval binding
+     loop @ y -> \(c : S1) -> c2t2c_loop' c @ y
+
+-- ----------------------------------------------------------------------
+-- tests
+
+-- p * p
+-- pp : IdP (<_> Torus) ptT ptT =
+--    <x> comp Torus (pathOneT{Torus} @ x) [(x=1) -> <y> pathOneT{Torus}@y]
+
+-- f :IdP (<x> IdP (<_> Torus) (pathTwoT{Torus}@x) (pathTwoT{Torus}@x) ) (<y> pathOneT{Torus}@y) (<y> pathOneT{Torus}@y) = 
+--   <x> <y> squareT{Torus} @ x @ y
+
+
+-- -- vertically compose two torus squares
+-- ff : IdP (<x> IdP (<_> Torus) (pathTwoT{Torus}@x) (pathTwoT{Torus}@x) ) pp pp = 
+--    <x> <y> comp Torus (squareT{Torus} @ x @ y) [(y=1) -> <y> squareT{Torus} @ x @ y]
+
+
+-- image_of_f : IdP (<x> IdP (<_> (_ : S1) * S1) (t2c (pathTwoT{Torus}@x)) (t2c (pathTwoT{Torus}@x)) ) (<x> t2c ((pathOneT{Torus}@x))) (<x> t2c ((pathOneT{Torus}@x))) = 
+--       <x> <y> t2c (f @ x @ y)
+
+-- image_of_ff : IdP (<x> IdP (<_> (_ : S1) * S1) (t2c (pathTwoT{Torus}@x)) (t2c (pathTwoT{Torus}@x)) ) (<x> t2c (pp @ x)) (<x> t2c (pp @ x)) = 
+--       <x> <y> t2c (ff @ x @ y)
+
+-- diag_of_image_of_ff : IdP (<_> (_ : S1) * S1) (base,base) (base,base)
+--   = <x> image_of_ff @ x @ x
+
+-- Type checking failed: path endpoints don't match for 
+-- got (<!0> comp (Torus) (pathOneT {Torus} @ !0) [ (!0 = 1) -> <!1> pathOneT {Torus} @ !1 ],
+--      <!0> comp (Torus) (pathOneT {Torus} @ !0) [ (!0 = 1) -> <!1> pathOneT {Torus} @ !1 ]), 
+-- but expected
+--  (<!0> comp (Torus) (pathOneT {Torus} @ !0) 
+--                    [ (!0 = 0) -> <!1> pathOneT {Torus} @ !1 ],
+--                        <!0> comp (Torus) (pathOneT {Torus} @ !0) 
+--                             [ (!0 = 0) -> <!1> pathOneT {Torus} @ !1 ])
+
+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
+
+-- funDep (A0 A1 :U) (p:Id U A0 A1) (u0:A0) (u1:A1) :
+--       Id U (Id A0 u0 (transport (<i>p@-i) u1)) (Id A1 (transport p u0) u1) =
+--  <i> Id (p @ i) (transport (<l> p @ (i/\l)) u0) (transport (<l> p @ (i\/-l)) u1)
+
+-- 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)]

diff --git a/experiments/torus.ctt b/experiments/torus.ctt
deleted file mode 100644 (file)
index 84d4c29..0000000
--- a/experiments/torus.ctt
+++ /dev/null
@@ -1,190 +0,0 @@
-module torus where
-
-import sigma
-import helix
-
-data Torus = ptT
-           | pathOneT <i> [ (i=0) -> ptT, (i=1) -> ptT ]
-           | pathTwoT <i> [ (i=0) -> ptT, (i=1) -> ptT ]
-           | squareT <i j> [ (i=0) -> pathOneT {Torus} @ j
-                           , (i=1) -> pathOneT {Torus} @ j
-                           , (j=0) -> pathTwoT {Torus} @ i
-                           , (j=1) -> pathTwoT {Torus} @ i ]
-
--- Torus = S1 * S1 proof
-
---                  pathTwoT x
---              ________________
---              |              |
---   pathOneT y | squareT x y  | pathOneT y
---              |              |
---              |              |
---              ________________
---                  pathTwoT x
-
--- pathOneT is (loop,refl)
--- pathTwoT is (refl,loop)
-
--- ----------------------------------------------------------------------
--- function from the torus to two circles
-
-t2c : Torus -> ((x : S1) * S1) = split
-  ptT -> (base,base)
-  pathOneT @ y -> (loop{S1} @ y, base)
-  pathTwoT @ x -> (base, loop{S1} @ x)
-  squareT @ x y -> (loop{S1} @ y, loop{S1} @ x)
-
--- ----------------------------------------------------------------------
--- function from two circles to the torus
-
--- if we had nested splits, we could write this like this:
--- c2t' : S1 -> S1 -> Torus = split
---   base -> split
---        base -> ptT
---        loop @ x -> pathTwoT{Torus} @ x
---   loop @ x -> split
---        base -> pathOneT{Torus} @ x
---        loop @ y -> squareT{Torus} @ y @ x
--- 
--- I tried doing this with helper functions
--- 
--- c2t' : S1 -> S1 -> Torus = split
---   base -> c2tbase where
---           c2tbase : S1 -> Torus = split 
---             base -> ptT
---             loop @ x -> pathTwoT{Torus} @ x
---   loop @ x -> c2t2 where 
---     c2tbase : S1 -> Torus = split
---        base -> pathOneT{Torus} @ x
---        loop @ y -> squareT{Torus} @ y @ x
--- 
--- but the faces don't work: want c2t2 <0/x> = c2t1 and similarly for 1.
--- I guess faces don't reduce on functions?
-
--- Instead, we can lift each branch into a helper function:
-
--- branch for base
-c2t_base : S1 -> Torus = split 
-  base -> ptT
-  loop @ x -> pathTwoT{Torus} @ x
-
--- branch for loop
--- 
--- I want to be able to do a split inside an interval abstraction:
---
--- c2t_loop : IdP (<_>S1 -> Torus) c2t_base c2t_base = 
---   <x> split
---         base -> pathOneT{Torus} @ x
---         loop @ y -> squareT{Torus} @ y @ x
--- 
--- but this doesn't seem possible?
--- 
--- One option would be to have split as a first-class term, rather
--- than something that only follows a definition.  
---
--- Alternatively, it would be enough if when something has an identity type, 
--- you could bind the dimension in the telescope somehow.
--- i.e. we could write this clausally as 
--- c2t_loop x base = pathOneT{Torus} @ x
--- c2t_loop x (loop @ y) = squareT{Torus} @ y @ x
-
--- Instead, we can use function extensionality to exchange the interval
--- variable and the circle variable, so that the thing we want to induct on 
--- is on the outside.  
-
-c2t_loop' : (c : S1) -> IdP (<_>Torus) (c2t_base c) (c2t_base c) = split
-   base -> < x > pathOneT{Torus} @ x
-   loop @ y -> < x > squareT{Torus} @ y @ x
-
--- use funext to exchange the interval variable and the S1 variable
-c2t_loop : IdP (<_>S1 -> Torus) c2t_base c2t_base =
-   <y> (\ (c : S1) -> (c2t_loop' c) @ y)
-
-c2t' : S1 -> S1 -> Torus = split
-  base -> c2t_base 
-  loop @ y -> c2t_loop @ y
-
-c2t (cs : ((_ : S1) * S1)) : Torus = c2t' cs.1 cs.2
-
-------------------------------------------------------------------------
--- first composite: induct and reflexivity! 
-
-t2c2t : (t : Torus) -> IdP (<_> Torus) (c2t (t2c t)) t = split 
-  ptT -> (<_> ptT)
-  pathOneT @ y -> (<_> pathOneT{Torus} @ y)
-  pathTwoT @ x -> (<_> pathTwoT{Torus} @ x)
-  squareT @ x y -> (<_> squareT{Torus} @ x @ y)
-
-------------------------------------------------------------------------
--- second composite: induct and reflexivity!
--- except we need to use the same tricks as in c2t to do the inner induction
-
-c2t2c_base : (c2 : S1) -> IdP (<_> (_ : S1) * S1) (t2c (c2t_base c2)) (base , c2) = split
-  base -> <_> (base , base)
-  loop @ y -> <_> (base , loop{S1} @ y)
-
--- the loop goal reduced using the defintional equalties, and with the two binders exchanged.
--- c2t' (loop @ y) c2 = (c2t_loop @ y c2) = c2t_loop' c2 @ y
-c2t2c_loop' : (c2 : S1) ->
-      IdP (<y> IdP (<_> (_ : S1) * S1) (t2c (c2t_loop @ y c2)) (loop{S1} @ y , c2))
-          (c2t2c_base c2)
-          (c2t2c_base c2) = split 
-    base -> <y> <_> (loop{S1}@y, base)
-    loop @ x -> <y> <_> (loop{S1} @ y, loop{S1} @ x)
-
-c2t2c : (c1 : S1) (c2 : S1) -> IdP (<_> (_ : S1) * S1) (t2c (c2t' c1 c2)) (c1 , c2) = split
-     base -> c2t2c_base
-                 -- again, I shouldn't need to do funext here;
-                 -- I should be able to do a split inside of an interval binding
-     loop @ y -> (\ (c : S1) -> c2t2c_loop' c @ y)
-
--- ----------------------------------------------------------------------
--- tests
-
--- p * p
-pp : IdP (<_> Torus) ptT ptT =
-   <x> comp Torus (pathOneT{Torus} @ x) [(x=1) -> <y> pathOneT{Torus}@y]
-
-f :IdP (<x> IdP (<_> Torus) (pathTwoT{Torus}@x) (pathTwoT{Torus}@x) ) (<y> pathOneT{Torus}@y) (<y> pathOneT{Torus}@y) = 
-  <x> <y> squareT{Torus} @ x @ y
-
-
--- vertically compose two torus squares
-ff : IdP (<x> IdP (<_> Torus) (pathTwoT{Torus}@x) (pathTwoT{Torus}@x) ) pp pp = 
-   <x> <y> comp Torus (squareT{Torus} @ x @ y) [(y=1) -> <y> squareT{Torus} @ x @ y]
-
-
-image_of_f : IdP (<x> IdP (<_> (_ : S1) * S1) (t2c (pathTwoT{Torus}@x)) (t2c (pathTwoT{Torus}@x)) ) (<x> t2c ((pathOneT{Torus}@x))) (<x> t2c ((pathOneT{Torus}@x))) = 
-      <x> <y> t2c (f @ x @ y)
-
-image_of_ff : IdP (<x> IdP (<_> (_ : S1) * S1) (t2c (pathTwoT{Torus}@x)) (t2c (pathTwoT{Torus}@x)) ) (<x> t2c (pp @ x)) (<x> t2c (pp @ x)) = 
-      <x> <y> t2c (ff @ x @ y)
-
-diag_of_image_of_ff : IdP (<_> (_ : S1) * S1) (base,base) (base,base)
-  = <x> image_of_ff @ x @ x
-
--- Type checking failed: path endpoints don't match for 
--- got (<!0> comp (Torus) (pathOneT {Torus} @ !0) [ (!0 = 1) -> <!1> pathOneT {Torus} @ !1 ],
---      <!0> comp (Torus) (pathOneT {Torus} @ !0) [ (!0 = 1) -> <!1> pathOneT {Torus} @ !1 ]), 
--- but expected
---  (<!0> comp (Torus) (pathOneT {Torus} @ !0) 
---                    [ (!0 = 0) -> <!1> pathOneT {Torus} @ !1 ],
---                        <!0> comp (Torus) (pathOneT {Torus} @ !0) 
---                             [ (!0 = 0) -> <!1> pathOneT {Torus} @ !1 ])
-
-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)]