From: Anders Mörtberg Date: Fri, 16 Oct 2015 15:47:20 +0000 (-0400) Subject: Patch and clean the torus example X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=a6acf8bad07e5133390f743bab0c75616fc630a7;p=cubicaltt.git Patch and clean the torus example --- diff --git a/examples/circle.ctt b/examples/circle.ctt index 126b319..59c608a 100644 --- a/examples/circle.ctt +++ b/examples/circle.ctt @@ -64,3 +64,10 @@ triv : loopS1 = base -- around the circle and then back is contractible: hmtpy : Id loopS1 ( base) ( loop{S1} @ (i /\ -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 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=0) -> ptT, (i=1) -> ptT ] + | pathTwoT [ (i=0) -> ptT, (i=1) -> ptT ] + | squareT [ (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 = + \(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 ( IdP (<_> and S1 S1) (t2c (c2t_loop @ y c2)) (loop1 @ y , c2)) + (c2t2c_base c2) + (c2t2c_base c2) = split + base -> <_> (loop1 @ y, base) + loop @ x -> <_> (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 = +-- comp Torus (pathOneT{Torus} @ x) [(x=1) -> pathOneT{Torus}@y] + +-- f :IdP ( IdP (<_> Torus) (pathTwoT{Torus}@x) (pathTwoT{Torus}@x) ) ( pathOneT{Torus}@y) ( pathOneT{Torus}@y) = +-- squareT{Torus} @ x @ y + + +-- -- vertically compose two torus squares +-- ff : IdP ( IdP (<_> Torus) (pathTwoT{Torus}@x) (pathTwoT{Torus}@x) ) pp pp = +-- comp Torus (squareT{Torus} @ x @ y) [(y=1) -> squareT{Torus} @ x @ y] + + +-- image_of_f : IdP ( IdP (<_> (_ : S1) * S1) (t2c (pathTwoT{Torus}@x)) (t2c (pathTwoT{Torus}@x)) ) ( t2c ((pathOneT{Torus}@x))) ( t2c ((pathOneT{Torus}@x))) = +-- t2c (f @ x @ y) + +-- image_of_ff : IdP ( IdP (<_> (_ : S1) * S1) (t2c (pathTwoT{Torus}@x)) (t2c (pathTwoT{Torus}@x)) ) ( t2c (pp @ x)) ( t2c (pp @ x)) = +-- t2c (ff @ x @ y) + +-- diag_of_image_of_ff : IdP (<_> (_ : S1) * S1) (base,base) (base,base) +-- = image_of_ff @ x @ x + +-- Type checking failed: path endpoints don't match for +-- got ( comp (Torus) (pathOneT {Torus} @ !0) [ (!0 = 1) -> pathOneT {Torus} @ !1 ], +-- comp (Torus) (pathOneT {Torus} @ !0) [ (!0 = 1) -> pathOneT {Torus} @ !1 ]), +-- but expected +-- ( comp (Torus) (pathOneT {Torus} @ !0) +-- [ (!0 = 0) -> pathOneT {Torus} @ !1 ], +-- comp (Torus) (pathOneT {Torus} @ !0) +-- [ (!0 = 0) -> 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) = 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 (p@-i) u1)) (Id A1 (transport p u0) u1) = +-- Id (p @ i) (transport ( p @ (i/\l)) u0) (transport ( p @ (i\/-l)) u1) + +-- loopTorusEqualsZZ : Id U loopT (and Z Z) = 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) = +-- comp U (lemIdAnd S1 S1 (base,base) (base,base) @ i) +-- [(i = 1) -> and (loopS1equalsZ @ j) (loopS1equalsZ @ j)] diff --git a/experiments/torus.ctt b/experiments/torus.ctt deleted file mode 100644 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=0) -> ptT, (i=1) -> ptT ] - | pathTwoT [ (i=0) -> ptT, (i=1) -> ptT ] - | squareT [ (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 = --- 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 = - (\ (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 ( IdP (<_> (_ : S1) * S1) (t2c (c2t_loop @ y c2)) (loop{S1} @ y , c2)) - (c2t2c_base c2) - (c2t2c_base c2) = split - base -> <_> (loop{S1}@y, base) - loop @ x -> <_> (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 = - comp Torus (pathOneT{Torus} @ x) [(x=1) -> pathOneT{Torus}@y] - -f :IdP ( IdP (<_> Torus) (pathTwoT{Torus}@x) (pathTwoT{Torus}@x) ) ( pathOneT{Torus}@y) ( pathOneT{Torus}@y) = - squareT{Torus} @ x @ y - - --- vertically compose two torus squares -ff : IdP ( IdP (<_> Torus) (pathTwoT{Torus}@x) (pathTwoT{Torus}@x) ) pp pp = - comp Torus (squareT{Torus} @ x @ y) [(y=1) -> squareT{Torus} @ x @ y] - - -image_of_f : IdP ( IdP (<_> (_ : S1) * S1) (t2c (pathTwoT{Torus}@x)) (t2c (pathTwoT{Torus}@x)) ) ( t2c ((pathOneT{Torus}@x))) ( t2c ((pathOneT{Torus}@x))) = - t2c (f @ x @ y) - -image_of_ff : IdP ( IdP (<_> (_ : S1) * S1) (t2c (pathTwoT{Torus}@x)) (t2c (pathTwoT{Torus}@x)) ) ( t2c (pp @ x)) ( t2c (pp @ x)) = - t2c (ff @ x @ y) - -diag_of_image_of_ff : IdP (<_> (_ : S1) * S1) (base,base) (base,base) - = image_of_ff @ x @ x - --- Type checking failed: path endpoints don't match for --- got ( comp (Torus) (pathOneT {Torus} @ !0) [ (!0 = 1) -> pathOneT {Torus} @ !1 ], --- comp (Torus) (pathOneT {Torus} @ !0) [ (!0 = 1) -> pathOneT {Torus} @ !1 ]), --- but expected --- ( comp (Torus) (pathOneT {Torus} @ !0) --- [ (!0 = 0) -> pathOneT {Torus} @ !1 ], --- comp (Torus) (pathOneT {Torus} @ !0) --- [ (!0 = 0) -> 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) = S1S1equalsTorus @ -i - -loopT : U = Id Torus ptT ptT - -loopTorusEqualsZZ : Id U loopT (and Z Z) = 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) = - comp U (lemIdAnd S1 S1 (base,base) (base,base) @ i) - [(i = 1) -> and (loopS1equalsZ @ j) (loopS1equalsZ @ j)]