minor stuff

homotopy/spectrum.hlean

@@ -673,6 +673,36 @@ set_option pp.coercions true
       exact sorry
     end /- TODO FOR SSS -/
 
+set_option pp.coercions true
+
+  definition ppi_assoc_compose_left {A : Type*} {B C D : A → Type*}
+    (f : Π (a : A), B a →* C a) (g : Π (a : A), C a →* D a)
+    : (ppi_compose_left g ∘* ppi_compose_left f) ~* ppi_compose_left (λ a, g a ∘* f a) :=
+  begin
+    fapply phomotopy.mk, 
+    intro h, fapply eq_of_ppi_homotopy,
+    fapply ppi_homotopy.mk,
+    intro a, reflexivity,
+    esimp, 
+    repeat exact sorry,
+  end
+
+  definition psquare_of_ppi_compose_left {A : Type*} {B C D E : A → Type*} 
+    {ftop : Π (a : A), B a →* C a} {fbot : Π (a : A), D a →* E a}
+    {fleft : Π (a : A), B a →* D a} {fright : Π (a : A), C a →* E a}
+    (psq : Π (a :A), psquare (ftop a) (fbot a) (fleft a) (fright a))
+    : psquare
+        (ppi_compose_left ftop)
+        (ppi_compose_left fbot)
+        (ppi_compose_left fleft)
+        (ppi_compose_left fright)
+    :=
+  begin
+    refine (ppi_assoc_compose_left ftop fright) ⬝* _ ⬝* (ppi_assoc_compose_left fleft fbot)⁻¹*,
+    refine eq_of_homotopy (λ a, eq_of_phomotopy (psq a)) ▸ phomotopy.rfl, 
+    -- the last step is probably an unnecessary application of function extensionality.
+  end
+
   definition spi_compose_left_botsq
     {N : succ_str} {A : Type*} {E F : A → gen_spectrum N} (f : Π a, (E a) →ₛ (F a)) (n : N)
     : psquare
@@ -682,6 +712,7 @@ set_option pp.coercions true
         (pequiv.to_pmap ppi_loop_pequiv⁻¹ᵉ*)
     :=
     begin
+--      fapply psquare_of_ppi_compose_left,
       exact sorry
     end /- TODO FOR SSS -/