--- /dev/null
+
+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 =
+-- <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)
+
+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))
+ (<x> helix ((compId S1 a b c p q) @ x))
+ (compId U (helix a) (helix b) (helix c) (<x> helix (p @ x)) (<x> helix (q @ x))) =
+ J S1 b (\ (c : S1) (q : Id S1 b c) ->
+ Id (Id U (helix a) (helix c))
+ (<x> helix ((compId S1 a b c p q) @ x))
+ (compId U (helix a) (helix b) (helix c) (<x> helix (p @ x)) (<x> helix (q @ x))))
+ (<_> (<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 (<x> helix (itLoopNeg n @ x)) (inr zero)) (inl n) = split
+ zero -> <_> inl zero
+ suc n -> compId Z (transport (<x> helix (comp (S1) (itLoopNeg n @ x) [ (x = 1) -> <y> loop {S1} @ -y ])) (inr zero))
+ (predZ (transport (<x> helix (itLoopNeg n @ x)) (inr zero)))
+ (predZ (inl n))
+ adjust
+ (<x> predZ (IH @ x))
+ -- FIXME: this says incompatible system, but isn't it the definition of compId
+ -- <x> comp Z (adjust @ x) [ (x = 1) -> (<x> predZ (IH @ x)) ]
+ where
+ IH : Id Z (transport (<x> helix (itLoopNeg n @ x)) (inr zero)) (inl n) = decode_encode_base_neg n
+
+ adjust : Id Z (transport (<x> helix (comp (S1) (itLoopNeg n @ x) [ (x = 1) -> <y> loop {S1} @ -y ])) (inr zero))
+ (predZ (transport (<x> helix (itLoopNeg n @ x)) (inr zero))) =
+ compId Z (transport (<x> helix (comp (S1) (itLoopNeg n @ x) [ (x = 1) -> <y> loop {S1} @ -y ])) (inr zero))
+ (transport (<x> (comp U (helix (itLoopNeg n @ x)) [ (x = 1) -> <y> helix (loop {S1} @ -y) ])) (inr zero))
+ (predZ (transport (<x> helix (itLoopNeg n @ x)) (inr zero)))
+ (<x> transport ((shouldBeDefinitional base base base (itLoopNeg n) (<y> loop{S1} @ -y)) @ x) (inr zero))
+ (transport_compId Z Z Z (<x> (helix (itLoopNeg n @ x))) (<y> helix (loop {S1} @ -y)) (inr zero))
+
+decode_encode_base_nonneg : (n : nat) -> Id Z (transport (<x> helix (itLoop n @ x)) (inr zero)) (inr n) = split
+ zero -> <_> inr zero
+ suc n -> compId Z (transport (<x> helix (comp (S1) (itLoop n @ x) [ (x = 1) -> <y> loop {S1} @ y ])) (inr zero))
+ (sucZ (transport (<x> helix (itLoop n @ x)) (inr zero)))
+ (sucZ (inr n))
+ adjust
+ (<x> sucZ (IH @ x)) where
+ IH : Id Z (transport (<x> helix (itLoop n @ x)) (inr zero)) (inr n) = decode_encode_base_nonneg n
+
+ adjust : Id Z (transport (<x> helix (comp (S1) (itLoop n @ x) [ (x = 1) -> <y> loop {S1} @ y ])) (inr zero))
+ (sucZ (transport (<x> helix (itLoop n @ x)) (inr zero))) =
+ compId Z (transport (<x> helix (comp (S1) (itLoop n @ x) [ (x = 1) -> <y> loop {S1} @ y ])) (inr zero))
+ (transport (<x> (comp U (helix (itLoop n @ x)) [ (x = 1) -> <y> helix (loop {S1} @ y) ])) (inr zero))
+ (sucZ (transport (<x> helix (itLoop n @ x)) (inr zero)))
+ (<x> transport ((shouldBeDefinitional base base base (itLoop n) (<y> loop{S1} @ y)) @ x) (inr zero))
+ (transport_compId Z Z Z (<x> (helix (itLoop n @ x))) (<y> 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 (<i> 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 =
+ <x> c2t (p.1 @ x, p.2@x)
+
+t2cloops (l : loopT) : (and loopS1 loopS1) =
+ (<x> ((t2c (l @ x)).1), <x> ((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 = <x> comp Torus (step3.1 @ x) [(x = 1) -> step3.2]
+ step5 : (and loopS1 loopS1) = (t2cloops step4)
+ step6 : and Z Z = transport (<i> 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
+-}
projects / cubicaltt.git / commitdiff