From: Dan Licata Date: Tue, 5 May 2015 15:42:15 +0000 (-0400) Subject: cleaned up mystery.ctt for inclusion in repository: move rest of Omega(S1) = Z to... X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=0cefb7e05b21430da73da1ad13599e8a637a058a;p=cubicaltt.git cleaned up mystery.ctt for inclusion in repository: move rest of Omega(S1) = Z to helix.ctt and import T = S1*S1 from torus.ctt --- diff --git a/examples/helix.ctt b/examples/helix.ctt index 1f166a1..cd9c127 100644 --- a/examples/helix.ctt +++ b/examples/helix.ctt @@ -50,6 +50,27 @@ decode : (x:S1) -> helix x -> Id S1 base x = split rem1 : Id (Z -> loopS1) (transport p loopIt) loopIt = \ (n:Z) -> (lemIt n)@j rem : IdP p loopIt loopIt = transport ( (funDepTr T T p loopIt loopIt)@-j) rem1 +encodeDecode : (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)) + +decodeEncodeBaseNeg : (n : nat) -> Id Z (transport ( helix (itLoopNeg n @ x)) (inr zero)) (inl n) = split + zero -> <_> inl zero + suc n -> predZ (decodeEncodeBaseNeg n @ x) + +decodeEncodeBaseNonneg : (n : nat) -> Id Z (transport ( helix (itLoop n @ x)) (inr zero)) (inr n) = split + zero -> <_> inr zero + suc n -> ( sucZ ( decodeEncodeBaseNonneg n @ x)) + +decodeEncodeBase : (n : Z) -> Id Z (encode base (decode base n)) n = split + inl n -> decodeEncodeBaseNeg n + inr n -> decodeEncodeBaseNonneg n + +loopS1equalsZ : Id U loopS1 Z = + isoId loopS1 Z (encode base) (decode base) decodeEncodeBase (encodeDecode base) + + + lemPropF (A:U)(P:A->U)(pP:(x:A) -> prop (P x))(a0 a1:A)(p:Id A a0 a1)(b0:P a0)(b1:P a1): IdS A P a0 a1 p b0 b1 = (pP (p @ i) (transport (P (p@i /\ j)) b0) (transport (P (p@i \/ -j)) b1)) @ i diff --git a/examples/mystery.ctt b/examples/mystery.ctt index d3b76f7..7a88129 100644 --- a/examples/mystery.ctt +++ b/examples/mystery.ctt @@ -6,217 +6,8 @@ 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 -> comp Z (adjust @ x) [ (x = 1) -> ( predZ (IH @ x)) ] -{- --- FIXME: for some reason writing the comp directly didn't work as I was writing the function, --- but writing compId did. --- but now it does work. not sure how to get back to the state where it didn't work; --- I think there were some holes in places. -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)) --} - 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))) = - (comp Z - (transport ((shouldBeDefinitional base base base (itLoopNeg n) ( loop{S1} @ -y)) @ x) (inr zero)) - [ (x=1) -> - (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 -> comp Z (adjust @ x) [ (x = 1) -> ( 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))) = - (comp Z - (transport ((shouldBeDefinitional base base base (itLoop n) ( loop{S1} @ y)) @ x) (inr zero)) - [(x=1) -> (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) +-- a function on numbers: +-- (1) start with (Z * Z) * (Z * Z) -- (2) (loopS1 * loopS1) * (loopS1 * loopS1) -- (3) loopT * loopT -- (4) compose them to a loopT