From 3881982774f9c60e7a920f7b8b9a816ed5905c33 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Wed, 7 Jun 2017 00:54:52 -0400
Subject: [PATCH] small changes to spectrum

---
 homotopy/smash.hlean    | 2 +-
 homotopy/spectrum.hlean | 9 +++++----
 2 files changed, 6 insertions(+), 5 deletions(-)

diff --git a/homotopy/smash.hlean b/homotopy/smash.hlean
index 4b6d875..82d5a98 100644
--- a/homotopy/smash.hlean
+++ b/homotopy/smash.hlean
@@ -5,7 +5,7 @@ import homotopy.smash types.pointed2 .pushout homotopy.red_susp
 open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber prod.ops wedge is_trunc
      function red_susp unit
 
-  /- To prove: Σ(X × Y) ≃ ΣX ∨ ΣY ∨ Σ(X ∧ Y) (?) (notation means suspension, wedge, smash) -/
+  /- To prove: Σ(X × Y) ≃ ΣX ∨ ΣY ∨ Σ(X ∧ Y) (notation means suspension, wedge, smash) -/
 
   /- To prove: Σ(X ∧ Y) ≃ X ★ Y (?) (notation means suspension, smash, join) -/
 
diff --git a/homotopy/spectrum.hlean b/homotopy/spectrum.hlean
index 953faf3..33dc6aa 100644
--- a/homotopy/spectrum.hlean
+++ b/homotopy/spectrum.hlean
@@ -397,16 +397,16 @@ namespace spectrum
     spectrify_type X n ≃* Ω (spectrify_type X (S n)) :=
   begin
     refine !pshift_equiv ⬝e* _,
-    refine _ ⬝e* !pseq_colim_loop⁻¹ᵉ*,
-    transitivity pseq_colim (λk, spectrify_type_fun' X (succ k) (S n +' k)), rotate 1,
-    refine pseq_colim_equiv_constant (λn, !ap1_pcompose⁻¹*),
+    transitivity pseq_colim (λk, spectrify_type_fun' X (succ k) (S n +' k)),
     fapply pseq_colim_pequiv,
     { intro n, apply loopn_pequiv_loopn, apply pequiv_ap X, apply succ_str.add_succ },
     { intro k, apply to_homotopy,
       refine !passoc⁻¹* ⬝* _, refine pwhisker_right _ (loopn_succ_in_inv_natural (succ k) _) ⬝* _,
       refine !passoc ⬝* _ ⬝* !passoc⁻¹*, apply pwhisker_left,
       refine !apn_pcompose⁻¹* ⬝* _ ⬝* !apn_pcompose, apply apn_phomotopy,
-      exact !glue_ptransport⁻¹* }
+      exact !glue_ptransport⁻¹* },
+    refine _ ⬝e* !pseq_colim_loop⁻¹ᵉ*,
+    refine pseq_colim_equiv_constant (λn, !ap1_pcompose⁻¹*),
   end
 
   definition spectrify [constructor] {N : succ_str} (X : gen_prespectrum N) : gen_spectrum N :=
@@ -431,6 +431,7 @@ namespace spectrum
       --pshift_equiv_pinclusion (spectrify_type_fun X n) 0
       refine _ ⬝v* _,
       rotate 1, exact pshift_equiv_pinclusion (spectrify_type_fun X n) 0,
+--      refine !passoc⁻¹* ⬝* pwhisker_left _ _ ⬝* _,
       exact sorry
 }
   end