simplified scompose

homotopy/pointed_cubes.hlean

@@ -45,3 +45,11 @@ definition psquare_of_pid_left_right {A B : Type*} {ftop : A →* B} {fbot : A
 psquare_of_phomotopy ((pid_pcompose ftop) ⬝* phtpy ⬝* ((pcompose_pid fbot)⁻¹*))
 
 print psquare_of_pid_left_right
+
+definition psquare_hcompose {A B C D E F : Type*} {ftop : A →* B} {fbot : D →* E} {fleft : A →* D} {fright : B →* E} {gtop : B →* C} {gbot : E →* F} {gright : C →* F} (psq_left : psquare ftop fbot fleft fright) (psq_right : psquare gtop gbot fright gright) : psquare (gtop ∘* ftop) (gbot ∘* fbot) fleft gright :=
+begin
+  fapply psquare_of_phomotopy,
+  refine (passoc gright gtop ftop)⁻¹* ⬝* _ ⬝* (passoc gbot fbot fleft)⁻¹*,
+  refine (pwhisker_right ftop psq_right) ⬝* (passoc gbot fright ftop) ⬝* _,
+  exact (pwhisker_left gbot psq_left),
+end

homotopy/spectrum.hlean

@@ -164,6 +164,11 @@ namespace spectrum
   definition scompose [trans] {N : succ_str} {X Y Z : gen_prespectrum N}
     (g : Y →ₛ Z) (f : X →ₛ Y) : X →ₛ Z :=
     smap.mk (λn, g n ∘* f n) 
+            (λ n, psquare_of_phtpy_bot 
+                    (ap1_pcompose (g (S n)) (f (S n))) 
+                    (psquare_hcompose (glue_square f n) (glue_square g n)))
+
+/-
       (λn, calc glue Z n ∘* to_fun g n ∘* to_fun f n
              ~* (glue Z n ∘* to_fun g n) ∘* to_fun f n                 : passoc
          ... ~* (Ω→(to_fun g (S n)) ∘* glue Y n) ∘* to_fun f n      : pwhisker_right (to_fun f n) (glue_square g n)
@@ -171,6 +176,7 @@ namespace spectrum
          ... ~* Ω→(to_fun g (S n)) ∘* (Ω→ (f (S n)) ∘* glue X n) : pwhisker_left (Ω→(to_fun g (S n))) (glue_square f n)
          ... ~* (Ω→(to_fun g (S n)) ∘* Ω→(f (S n))) ∘* glue X n  : passoc
          ... ~* Ω→(to_fun g (S n) ∘* to_fun f (S n)) ∘* glue X n : pwhisker_right (glue X n) (ap1_pcompose _ _))
+-/
 
   infixr ` ∘ₛ `:60 := scompose