From: Dan Licata Date: Sat, 2 May 2015 14:45:09 +0000 (-0400) Subject: use synthetic homotopy theory to get a function on numbers X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=9eeb750eefe9edf615cad5b05bff92fb0edf318b;p=cubicaltt.git use synthetic homotopy theory to get a function on numbers --- diff --git a/examples/mystery.ctt b/examples/mystery.ctt new file mode 100644 index 0000000..740517e --- /dev/null +++ b/examples/mystery.ctt @@ -0,0 +1,279 @@ + +module mystery where + +import prelude +import circle +import helix +import torus + +-- ---------------------------------------------------------------------- +-- torus is a product of two circles +-- ---------------------------------------------------------------------- + +-- 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) + +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 + + + +-- ---------------------------------------------------------------------- +-- part of Omega(S1) = Z is in helix.ctt, this is the rest +-- ---------------------------------------------------------------------- + +transport_compId (A : U) (B : U) (C : U) (p : Id U A B) (q : Id U B C) (a : A) + : Id C (transport (compId U A B C p q) a) (transport q (transport p a)) = + J U B (\ (C : U) (q : Id U B C) -> + Id C (transport (compId U A B C p q) a) (transport q (transport p a))) + (<_> (transport p a)) C q + +-- FIXME: (1) I think this should be definitional: it's a split on a comp +-- (2) I tried to write this using comp instead of compId and got some "infer" errors +shouldBeDefinitional (a : S1) (b : S1) (c : S1) (p : Id S1 a b) (q : Id S1 b c) : + Id (Id U (helix a) (helix c)) + ( helix ((compId S1 a b c p q) @ x)) + (compId U (helix a) (helix b) (helix c) ( helix (p @ x)) ( helix (q @ x))) = + J S1 b (\ (c : S1) (q : Id S1 b c) -> + Id (Id U (helix a) (helix c)) + ( helix ((compId S1 a b c p q) @ x)) + (compId U (helix a) (helix b) (helix c) ( helix (p @ x)) ( helix (q @ x)))) + (<_> ( helix (p @ x))) c q + +encode_decode : (c : S1) (p : Id S1 base c) -> Id (Id S1 base c) (decode c (encode c p)) p = + J S1 base (\ (c : S1) (p : Id S1 base c) -> Id (Id S1 base c) (decode c (encode c p)) p) + (<_> (<_> base)) + +decode_encode_base_neg : (n : nat) -> Id Z (transport ( helix (itLoopNeg n @ x)) (inr zero)) (inl n) = split + zero -> <_> inl zero + suc n -> compId Z (transport ( helix (comp (S1) (itLoopNeg n @ x) [ (x = 1) -> loop {S1} @ -y ])) (inr zero)) + (predZ (transport ( helix (itLoopNeg n @ x)) (inr zero))) + (predZ (inl n)) + adjust + ( predZ (IH @ x)) + -- FIXME: this says incompatible system, but isn't it the definition of compId + -- comp Z (adjust @ x) [ (x = 1) -> ( predZ (IH @ x)) ] + where + IH : Id Z (transport ( helix (itLoopNeg n @ x)) (inr zero)) (inl n) = decode_encode_base_neg n + + adjust : Id Z (transport ( helix (comp (S1) (itLoopNeg n @ x) [ (x = 1) -> loop {S1} @ -y ])) (inr zero)) + (predZ (transport ( helix (itLoopNeg n @ x)) (inr zero))) = + compId Z (transport ( helix (comp (S1) (itLoopNeg n @ x) [ (x = 1) -> loop {S1} @ -y ])) (inr zero)) + (transport ( (comp U (helix (itLoopNeg n @ x)) [ (x = 1) -> helix (loop {S1} @ -y) ])) (inr zero)) + (predZ (transport ( helix (itLoopNeg n @ x)) (inr zero))) + ( transport ((shouldBeDefinitional base base base (itLoopNeg n) ( loop{S1} @ -y)) @ x) (inr zero)) + (transport_compId Z Z Z ( (helix (itLoopNeg n @ x))) ( helix (loop {S1} @ -y)) (inr zero)) + +decode_encode_base_nonneg : (n : nat) -> Id Z (transport ( helix (itLoop n @ x)) (inr zero)) (inr n) = split + zero -> <_> inr zero + suc n -> compId Z (transport ( helix (comp (S1) (itLoop n @ x) [ (x = 1) -> loop {S1} @ y ])) (inr zero)) + (sucZ (transport ( helix (itLoop n @ x)) (inr zero))) + (sucZ (inr n)) + adjust + ( sucZ (IH @ x)) where + IH : Id Z (transport ( helix (itLoop n @ x)) (inr zero)) (inr n) = decode_encode_base_nonneg n + + adjust : Id Z (transport ( helix (comp (S1) (itLoop n @ x) [ (x = 1) -> loop {S1} @ y ])) (inr zero)) + (sucZ (transport ( helix (itLoop n @ x)) (inr zero))) = + compId Z (transport ( helix (comp (S1) (itLoop n @ x) [ (x = 1) -> loop {S1} @ y ])) (inr zero)) + (transport ( (comp U (helix (itLoop n @ x)) [ (x = 1) -> helix (loop {S1} @ y) ])) (inr zero)) + (sucZ (transport ( helix (itLoop n @ x)) (inr zero))) + ( transport ((shouldBeDefinitional base base base (itLoop n) ( loop{S1} @ y)) @ x) (inr zero)) + (transport_compId Z Z Z ( (helix (itLoop n @ x))) ( helix (loop {S1} @ y)) (inr zero)) + +decode_encode_base : (n : Z) -> Id Z (encode base (decode base n)) n = split + inl n -> decode_encode_base_neg n + inr n -> decode_encode_base_nonneg n + +loopS1equalsZ : IdP (<_>U) loopS1 Z = + isoId loopS1 Z (encode base) (decode base) decode_encode_base (encode_decode base) + + +-- ---------------------------------------------------------------------- +-- use them to get a function on numbers +-- ---------------------------------------------------------------------- + +-- (1) (Z * Z) * (Z * Z) +-- (2) (loopS1 * loopS1) * (loopS1 * loopS1) +-- (3) loopT * loopT +-- (4) compose them to a loopT +-- (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 ( and (and (loopS1equalsZ @ -i) (loopS1equalsZ @ -i)) (and (loopS1equalsZ @ -i) (loopS1equalsZ @ -i))) input + +-- could do this with transport too but would have to prove the equivalence +c2t_on_loops (p : (and loopS1 loopS1)) : loopT = + c2t (p.1 @ x, p.2@x) + +t2cloops (l : loopT) : (and loopS1 loopS1) = + ( ((t2c (l @ x)).1), ((t2c (l @ x)).2)) + +mystery (input : (and (and Z Z) (and Z Z))) : and Z Z = + step6 + where + step2 : and (and loopS1 loopS1) (and loopS1 loopS1) = Zs_to_loopS1s input + step3 : (and loopT loopT) = (c2t_on_loops step2.1, c2t_on_loops step2.2) + step4 : loopT = comp Torus (step3.1 @ x) [(x = 1) -> step3.2] + step5 : (and loopS1 loopS1) = (t2cloops step4) + step6 : and Z Z = transport ( and (loopS1equalsZ @ i) (loopS1equalsZ @ i)) step5 + +oneZ : Z = sucZ zeroZ +twoZ : Z = sucZ (oneZ) +threeZ : Z = sucZ twoZ +fourZ : Z = sucZ threeZ +fiveZ : Z = sucZ fourZ +sixZ : Z = sucZ sixZ + +test0 : Id (and Z Z) (mystery ((zeroZ,oneZ),(twoZ,threeZ))) (twoZ,fourZ) = + <_> (twoZ,fourZ) + +test1 : Id (and Z Z) (mystery ((oneZ,twoZ),(twoZ,threeZ))) (threeZ,fiveZ) = + <_> (threeZ,fiveZ) + +test1' : Id (and Z Z) (mystery ((twoZ,threeZ),(oneZ,twoZ))) (threeZ,fiveZ) = + <_> (threeZ,fiveZ) + +test2 : Id (and Z Z) (mystery ((oneZ,twoZ),(threeZ,threeZ))) (fourZ,fiveZ) = + <_> (fourZ,fiveZ) + +test3 : Id (and Z Z) (mystery ((twoZ,twoZ),(threeZ,threeZ))) (fiveZ,fiveZ) = + <_> (fiveZ,fiveZ) + +{- +test4 : Id (and Z Z) (mystery ((oneZ,twoZ),(threeZ,fourZ))) (fourZ,sixZ) = + <_> (fourZ,sixZ) +FIXME: + Stack space overflow + Use `+RTS -Ksize -RTS' to increase it. + runs out of stack space with 900MB stack +-}