From 6378a34fa6f48b9595a114a5987e5e528683d37a Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Sat, 8 Jul 2017 11:41:57 +0100
Subject: [PATCH] minor stuff

---
 homotopy/spectrum.hlean | 31 +++++++++++++++++++++++++++++++
 1 file changed, 31 insertions(+)

diff --git a/homotopy/spectrum.hlean b/homotopy/spectrum.hlean
index 79a1b0a..6f6aac1 100644
--- a/homotopy/spectrum.hlean
+++ b/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 -/