small changes to spectrum

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) -/
 

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