michael/Spectral
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

simplify szero

Browse source
This commit is contained in:
Egbert Rijke 2017-07-01 15:42:49 +01:00
parent dd18b3a72a
commit ed2ff9f113
1 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
homotopy/spectrum.hlean
View file

@ -182,9 +182,14 @@ namespace spectrum
definition szero [constructor] {N : succ_str} (E F : gen_prespectrum N) : E →ₛ F := definition szero [constructor] {N : succ_str} (E F : gen_prespectrum N) : E →ₛ F :=
smap.mk (λn, pconst (E n) (F n)) smap.mk (λn, pconst (E n) (F n))
(λn, psquare_of_phtpy_bot (ap1_pconst (E (S n)) (F (S n)))
(psquare_of_pconst_top_bot (glue E n) (glue F n)))
/-
(λn, calc glue F n ∘* pconst (E n) (F n) ~* pconst (E n) (Ω(F (S n))) : pcompose_pconst (λn, calc glue F n ∘* pconst (E n) (F n) ~* pconst (E n) (Ω(F (S n))) : pcompose_pconst
... ~* pconst (Ω(E (S n))) (Ω(F (S n))) ∘* glue E n : pconst_pcompose ... ~* pconst (Ω(E (S n))) (Ω(F (S n))) ∘* glue E n : pconst_pcompose
... ~* Ω→(pconst (E (S n)) (F (S n))) ∘* glue E n : pwhisker_right (glue E n) (ap1_pconst _ _)) ... ~* Ω→(pconst (E (S n)) (F (S n))) ∘* glue E n : pwhisker_right (glue E n) (ap1_pconst _ _))
-/
definition stransport [constructor] {N : succ_str} {A : Type} {a a' : A} (p : a = a') definition stransport [constructor] {N : succ_str} {A : Type} {a a' : A} (p : a = a')
(E : A → gen_prespectrum N) : E a →ₛ E a' := (E : A → gen_prespectrum N) : E a →ₛ E a' :=