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 -> <x> comp Z (adjust @ x) [ (x = 1) -> (<x> 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 (<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))
--}
- 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))) =
- <x> (comp Z
- (transport ((shouldBeDefinitional base base base (itLoopNeg n) (<y> loop{S1} @ -y)) @ x) (inr zero))
- [ (x=1) ->
- (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 -> <x> comp Z (adjust @ x) [ (x = 1) -> (<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))) =
- <x> (comp Z
- (transport ((shouldBeDefinitional base base base (itLoop n) (<y> loop{S1} @ y)) @ x) (inr zero))
- [(x=1) -> (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)
+-- 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
projects / cubicaltt.git / commitdiff