on colim.elim o pinclusion, and corollary on spectra

colim.hlean

@@ -399,8 +399,8 @@ namespace seq_colim
   equiv.mk _ !is_equiv_seq_colim_rec
   end functor
 
-  definition pseq_colim.elim' [constructor] {A : ℕ → Type*} {B : Type*} {f : Π{n}, A n →* A (n+1)}
+  definition pseq_colim.elim' [constructor] {A : ℕ → Type*} {B : Type*} {f : Πn, A n →* A (n+1)}
-    (g : Πn, A n →* B) (p : Πn, g (n+1) ∘* f ~ g n) : pseq_colim @f →* B :=
+    (g : Πn, A n →* B) (p : Πn, g (n+1) ∘* f n ~ g n) : pseq_colim f →* B :=
   begin
     fapply pmap.mk,
     { intro x, induction x with n a n a,
@@ -409,10 +409,38 @@ namespace seq_colim
     { esimp, apply respect_pt }
   end
 
-  definition pseq_colim.elim [constructor] {A : ℕ → Type*} {B : Type*} {f : Π{n}, A n →* A (n+1)}
+  definition pseq_colim.elim [constructor] {A : ℕ → Type*} {B : Type*} {f : Πn, A n →* A (n+1)}
-    (g : Πn, A n →* B) (p : Πn, g (n+1) ∘* f ~* g n) : pseq_colim @f →* B :=
+    (g : Πn, A n →* B) (p : Πn, g (n+1) ∘* f n ~* g n) : pseq_colim @f →* B :=
   pseq_colim.elim' g p
 
+  definition pseq_colim.elim_pinclusion {A : ℕ → Type*} {B : Type*} {f : Πn, A n →* A (n+1)}
+    (g : Πn, A n →* B) (p : Πn, g (n+1) ∘* f n ~* g n) (n : ℕ) :
+  pseq_colim.elim g p ∘* pinclusion f n ~* g n :=
+  begin
+    refine phomotopy.mk phomotopy.rfl _,
+    refine !idp_con ⬝ _,
+    esimp,
+    induction n with n IH,
+    { esimp, esimp[inclusion_pt], exact !idp_con⁻¹ },
+    { esimp, esimp[inclusion_pt],
+      rewrite ap_con, rewrite ap_con,
+      rewrite elim_glue,
+      rewrite [-ap_inv],
+      rewrite [-ap_compose'], esimp,
+      rewrite [(eq_con_inv_of_con_eq (!to_homotopy_pt))],
+      rewrite [IH],
+      rewrite [con_inv],
+      rewrite [-+con.assoc],
+      refine _ ⬝ whisker_right _ !con.assoc⁻¹,
+      rewrite [con.left_inv], esimp,
+      refine _ ⬝ !con.assoc⁻¹,
+      rewrite [con.left_inv], esimp,
+      rewrite [ap_inv],
+      rewrite [-con.assoc],
+      refine !idp_con⁻¹ ⬝ whisker_right _ !con.left_inv⁻¹,
+    }
+  end
+
   definition prep0 [constructor] {A : ℕ → Type*} (f : pseq_diagram A) (k : ℕ) : A 0 →* A k :=
   pmap.mk (rep0 (λn x, f x) k)
           begin induction k with k p, reflexivity, exact ap (@f k) p ⬝ !respect_pt end

homotopy/spectrum.hlean

@@ -477,11 +477,10 @@ namespace spectrum
     }
   end
 
-  definition spectrify.elim {N : succ_str} {X : gen_prespectrum N} {Y : gen_spectrum N}
+  definition spectrify.elim_n {N : succ_str} {X : gen_prespectrum N} {Y : gen_spectrum N}
-    (f : X →ₛ Y) : spectrify X →ₛ Y :=
+    (f : X →ₛ Y) (n : N) : (spectrify X) n →* Y n :=
   begin
-    fapply smap.mk,
+    fapply pseq_colim.elim,
-    { intro n, fapply pseq_colim.elim,
     { intro k, refine !equiv_gluen⁻¹ᵉ* ∘* apn k (f (n +' k)) },
     { intro k, refine !passoc ⬝* pwhisker_right _ !equiv_gluen_inv_succ ⬝* _,
       refine !passoc ⬝* _, apply pwhisker_left,
@@ -495,10 +494,24 @@ namespace spectrum
       refine apn_psquare k _,
       refine pwhisker_right _ _  ⬝* psquare_of_phomotopy !smap.glue_square,
       exact !pmap_eta⁻¹*
-      }},
+    }
+  end
+
+  definition spectrify.elim {N : succ_str} {X : gen_prespectrum N} {Y : gen_spectrum N}
+    (f : X →ₛ Y) : spectrify X →ₛ Y :=
+  begin
+    fapply smap.mk,
+    { intro n, exact spectrify.elim_n f n },
     { intro n, exact sorry }
   end
 
+  definition phomotopy_spectrify.elim {N : succ_str} {X : gen_prespectrum N} {Y : gen_spectrum N}
+    (f : X →ₛ Y) (n : N) : spectrify.elim_n f n ∘* spectrify_map n ~* f n :=
+  begin
+    refine pseq_colim.elim_pinclusion _ _ 0 ⬝* _,
+    exact !pid_pcompose
+  end
+
   definition spectrify_fun {N : succ_str} {X Y : gen_prespectrum N} (f : X →ₛ Y) : spectrify X →ₛ spectrify Y :=
   spectrify.elim ((@spectrify_map _ Y) ∘ₛ f)