diff --git a/homotopy/EM.hlean b/homotopy/EM.hlean
index aa95281..03eb5c3 100644
--- a/homotopy/EM.hlean
+++ b/homotopy/EM.hlean
@@ -570,4 +570,11 @@ namespace EM
     abstract (EMadd1_functor_gcompose φ φ⁻¹ᵍ n)⁻¹* ⬝* EMadd1_functor_phomotopy proof right_inv φ qed n ⬝*
              EMadd1_functor_gid H n end
 
+  definition EM_pequiv_EM (n : ℕ) {G H : AbGroup} (φ : G ≃g H) : K G n ≃* K H n :=
+  begin
+    cases n with n,
+    { exact pequiv_of_isomorphism φ },
+    { exact EMadd1_pequiv_EMadd1 n φ }
+  end
+
 end EM
diff --git a/homotopy/cohomology.hlean b/homotopy/cohomology.hlean
index 8c25b70..e1d9fdc 100644
--- a/homotopy/cohomology.hlean
+++ b/homotopy/cohomology.hlean
@@ -20,31 +20,64 @@ namespace cohomology
 definition cohomology (X : Type*) (Y : spectrum) (n : ℤ) : AbGroup :=
 AbGroup_trunc_pmap X (Y (n+2))
 
-definition parametrized_cohomology {X : Type*} (Y : X → spectrum) (n : ℤ) : AbGroup :=
-AbGroup_trunc_ppi (λx, Y x (n+2))
-
 definition ordinary_cohomology [reducible] (X : Type*) (G : AbGroup) (n : ℤ) : AbGroup :=
 cohomology X (EM_spectrum G) n
 
 definition ordinary_cohomology_Z [reducible] (X : Type*) (n : ℤ) : AbGroup :=
 ordinary_cohomology X agℤ n
 
-notation `H^` n `[`:0 X:0 `, ` Y:0 `]`:0 := cohomology X Y n
-notation `H^` n `[`:0 X:0 `]`:0 := ordinary_cohomology_Z X n
+definition unreduced_cohomology (X : Type) (Y : spectrum) (n : ℤ) : AbGroup :=
+cohomology X₊ Y n
+
+definition unreduced_ordinary_cohomology [reducible] (X : Type) (G : AbGroup) (n : ℤ) : AbGroup :=
+unreduced_cohomology X (EM_spectrum G) n
+
+definition unreduced_ordinary_cohomology_Z [reducible] (X : Type) (n : ℤ) : AbGroup :=
+unreduced_ordinary_cohomology X agℤ n
+
+definition parametrized_cohomology {X : Type*} (Y : X → spectrum) (n : ℤ) : AbGroup :=
+AbGroup_trunc_ppi (λx, Y x (n+2))
+
+definition ordinary_parametrized_cohomology [reducible] {X : Type*} (G : X → AbGroup) (n : ℤ) :
+  AbGroup :=
+parametrized_cohomology (λx, EM_spectrum (G x)) n
+
+definition unreduced_parametrized_cohomology {X : Type} (Y : X → spectrum) (n : ℤ) : AbGroup :=
+@parametrized_cohomology X₊ (λx, option.cases_on x sunit Y) n
+
+definition unreduced_ordinary_parametrized_cohomology [reducible] {X : Type} (G : X → AbGroup)
+  (n : ℤ) : AbGroup :=
+unreduced_parametrized_cohomology (λx, EM_spectrum (G x)) n
+
+notation `H^` n `[`:0 X:0 `, ` Y:0 `]`:0   := cohomology X Y n
+notation `oH^` n `[`:0 X:0 `, ` G:0 `]`:0  := ordinary_cohomology X G n
+notation `H^` n `[`:0 X:0 `]`:0            := ordinary_cohomology_Z X n
+notation `uH^` n `[`:0 X:0 `, ` Y:0 `]`:0  := unreduced_cohomology X Y n
+notation `uoH^` n `[`:0 X:0 `, ` G:0 `]`:0 := unreduced_ordinary_cohomology X G n
+notation `uH^` n `[`:0 X:0 `]`:0           := unreduced_ordinary_cohomology_Z X n
 notation `pH^` n `[`:0 binders `, ` r:(scoped Y, parametrized_cohomology Y n) `]`:0 := r
+notation `opH^` n `[`:0 binders `, ` r:(scoped G, ordinary_parametrized_cohomology G n) `]`:0 := r
+notation `upH^` n `[`:0 binders `, ` r:(scoped Y, unreduced_parametrized_cohomology Y n) `]`:0 := r
+notation `uopH^` n `[`:0 binders `, ` r:(scoped G, unreduced_ordinary_parametrized_cohomology G n) `]`:0 := r
 
 -- check H^3[S¹*,EM_spectrum agℤ]
 -- check H^3[S¹*]
 -- check pH^3[(x : S¹*), EM_spectrum agℤ]
 
 /- an alternate definition of cohomology -/
-definition cohomology_equiv_shomotopy_group_cotensor (X : Type*) (Y : spectrum) (n : ℤ) :
+definition cohomology_equiv_shomotopy_group_sp_cotensor (X : Type*) (Y : spectrum) (n : ℤ) :
   H^n[X, Y] ≃ πₛ[-n] (sp_cotensor X Y) :=
 trunc_equiv_trunc 0 (!pfunext ⬝e loop_pequiv_loop !pfunext ⬝e loopn_pequiv_loopn 2
   (pequiv_of_eq (ap (λn, ppmap X (Y n)) (add.comm n 2 ⬝ ap (add 2) !neg_neg⁻¹))))
 
-definition unpointed_cohomology (X : Type) (Y : spectrum) (n : ℤ) : AbGroup :=
-cohomology X₊ Y n
+definition cohomology_isomorphism_shomotopy_group_sp_cotensor (X : Type*) (Y : spectrum) {n m : ℤ}
+  (p : -m = n) : H^n[X, Y] ≃g πₛ[m] (sp_cotensor X Y) :=
+sorry
+
+definition parametrized_cohomology_isomorphism_shomotopy_group_spi {X : Type*} (Y : X → spectrum)
+  {n m : ℤ} (p : -m = n) : pH^n[(x : X), Y x] ≃g πₛ[m] (spi X Y) :=
+sorry
+
 
 /- functoriality -/
 
@@ -81,6 +114,23 @@ definition cohomology_isomorphism_refl (X : Type*) (Y : spectrum) (n : ℤ) (x :
   cohomology_isomorphism (pequiv.refl X) Y n x = x :=
 !Group_trunc_pmap_isomorphism_refl
 
+definition cohomology_isomorphism_right (X : Type*) {Y Y' : spectrum} (e : Πn, Y n ≃* Y' n) (n : ℤ)
+   : H^n[X, Y] ≃g H^n[X, Y'] :=
+sorry
+
+definition parametrized_cohomology_isomorphism_right (X : Type*) {Y Y' : X → spectrum}
+  (e : Πx n, Y x n ≃* Y' x n) (n : ℤ)
+   : pH^n[(x : X), Y x] ≃g pH^n[(x : X), Y' x] :=
+sorry
+
+definition ordinary_cohomology_isomorphism_right (X : Type*) {G G' : AbGroup} (e : G ≃g G')
+  (n : ℤ) : oH^n[X, G] ≃g oH^n[X, G'] :=
+cohomology_isomorphism_right X (EM_spectrum_pequiv e) n
+
+definition ordinary_parametrized_cohomology_isomorphism_right (X : Type*) {G G' : X → AbGroup}
+  (e : Πx, G x ≃g G' x) (n : ℤ) : opH^n[(x : X), G x] ≃g opH^n[(x : X), G' x] :=
+parametrized_cohomology_isomorphism_right X (λx, EM_spectrum_pequiv (e x)) n
+
 /- suspension axiom -/
 
 definition cohomology_psusp_2 (Y : spectrum) (n : ℤ) :
@@ -169,6 +219,11 @@ theorem EM_dimension (G : AbGroup) (n : ℤ) (H : n ≠ 0) :
   (equiv_of_isomorphism (cohomology_isomorphism (pequiv_plift pbool) _ _)))
   (EM_dimension' G n H)
 
+open group algebra
+theorem ordinary_cohomology_pbool (G : AbGroup) : ordinary_cohomology pbool G 0 ≃g G :=
+sorry
+--isomorphism_of_equiv (trunc_equiv_trunc 0 (ppmap_pbool_pequiv _ ⬝e _)  ⬝e !trunc_equiv) sorry
+
 /- cohomology theory -/
 
 structure cohomology_theory.{u} : Type.{u+1} :=
diff --git a/homotopy/serre.hlean b/homotopy/serre.hlean
index eb19084..de278ea 100644
--- a/homotopy/serre.hlean
+++ b/homotopy/serre.hlean
@@ -1,9 +1,12 @@
-import ..algebra.module_exact_couple .strunc
+import ..algebra.module_exact_couple .strunc .cohomology
 
 open eq spectrum trunc is_trunc pointed int EM algebra left_module fiber lift equiv is_equiv
+     cohomology group sigma unit
+set_option pp.binder_types true
 
 /- Eilenberg MacLane spaces are the fibers of the Postnikov system of a type -/
 
+namespace pointed
 definition postnikov_map [constructor] (A : Type*) (n : ℕ₋₂) : ptrunc (n.+1) A →* ptrunc n A :=
 ptrunc.elim (n.+1) !ptr
 
@@ -62,6 +65,10 @@ begin
 end,
 this⁻¹ᵛ*
 
+end pointed open pointed
+
+namespace spectrum
+
 definition is_strunc_strunc_pred (X : spectrum) (k : ℤ) : is_strunc k (strunc (k - 1) X) :=
 λn, @(is_trunc_of_le _ (maxm2_monotone (add_le_add_right (sub_one_le k) n))) !is_strunc_strunc
 
@@ -69,10 +76,11 @@ definition postnikov_smap [constructor] (X : spectrum) (k : ℤ) :
   strunc k X →ₛ strunc (k - 1) X :=
 strunc_elim (str (k - 1) X) (is_strunc_strunc_pred X k)
 
-definition postnikov_smap_phomotopy [constructor] (X : spectrum) (k : ℤ) (n : ℤ) :
-  postnikov_smap X k n ~* postnikov_map (X n) (maxm2 (k - 1 + n)) ∘*
-  sorry :=
-sorry
+definition pfiber_postnikov_smap (A : spectrum) (n : ℤ) (k : ℤ) :
+  pfiber (postnikov_smap A n k) ≃* EM_spectrum (πₛ[n] A) k :=
+begin
+  exact sorry
+end
 
 section atiyah_hirzebruch
   parameters {X : Type*} (Y : X → spectrum) (s₀ : ℤ) (H : Πx, is_strunc s₀ (Y x))
@@ -80,16 +88,95 @@ section atiyah_hirzebruch
   definition atiyah_hirzebruch_exact_couple : exact_couple rℤ Z2 :=
   @exact_couple_sequence (λs, strunc s (spi X Y)) (postnikov_smap (spi X Y))
 
+  definition atiyah_hirzebruch_ub ⦃s n : ℤ⦄ (Hs : s ≤ n - 1) :
+    is_contr (πₛ[n] (strunc s (spi X Y))) :=
+  begin
+    apply trivial_shomotopy_group_of_is_strunc,
+      apply is_strunc_strunc,
+    exact lt_of_le_sub_one Hs
+  end
+
+  include H
+  definition atiyah_hirzebruch_lb ⦃s n : ℤ⦄ (Hs : s ≥ s₀ + 1) :
+    is_equiv (postnikov_smap (spi X Y) s n) :=
+  begin
+    have H2 : is_strunc s₀ (spi X Y), from is_strunc_spi _ _ H,
+    refine is_equiv_of_equiv_of_homotopy
+      (ptrunc_pequiv_ptrunc_of_is_trunc _ _ (H2 n)) _,
+    { apply maxm2_monotone, apply add_le_add_right, exact le.trans !le_add_one Hs },
+    { apply maxm2_monotone, apply add_le_add_right, exact le_sub_one_of_lt Hs },
+    refine @trunc.rec _ _ _ _ _,
+    { intro x, apply is_trunc_eq,
+      assert H3 : maxm2 (s - 1 + n) ≤ (maxm2 (s + n)).+1,
+      { refine trunc_index.le_succ (maxm2_monotone (le.trans (le_of_eq !add.right_comm)
+                                                             !sub_one_le)) },
+      exact @is_trunc_of_le _ _ _ H3 !is_trunc_trunc },
+    intro a, reflexivity
+  end
+
   definition is_bounded_atiyah_hirzebruch : is_bounded atiyah_hirzebruch_exact_couple :=
-  is_bounded_sequence _ s₀ (λn, n - 1)
+  is_bounded_sequence _ s₀ (λn, n - 1) atiyah_hirzebruch_lb atiyah_hirzebruch_ub
+
+  definition atiyah_hirzebruch_convergence' :
+    (λn s, πₛ[n] (sfiber (postnikov_smap (spi X Y) s))) ⟹ᵍ (λn, πₛ[n] (strunc s₀ (spi X Y))) :=
+  converges_to_sequence _ s₀ (λn, n - 1) atiyah_hirzebruch_lb atiyah_hirzebruch_ub
+
+  lemma spi_EM_spectrum (k s : ℤ) :
+    EM_spectrum (πₛ[s] (spi X Y)) k ≃* spi X (λx, EM_spectrum (πₛ[s] (Y x))) k :=
+  sorry
+
+  definition atiyah_hirzebruch_convergence :
+    (λn s, opH^-n[(x : X), πₛ[s] (Y x)]) ⟹ᵍ (λn, pH^-n[(x : X), Y x]) :=
+  converges_to_g_isomorphism atiyah_hirzebruch_convergence'
     begin
-      intro s n H,
-      exact sorry
+      intro n s,
+      refine _ ⬝g (parametrized_cohomology_isomorphism_shomotopy_group_spi _ idp)⁻¹ᵍ,
+      apply shomotopy_group_isomorphism_of_pequiv, intro k,
+      refine pfiber_postnikov_smap (spi X Y) s k ⬝e* _,
+      apply spi_EM_spectrum
     end
     begin
-      intro s n H, apply trivial_shomotopy_group_of_is_strunc,
-        apply is_strunc_strunc,
-      exact lt_of_le_sub_one H,
+      intro n,
+      refine _ ⬝g (parametrized_cohomology_isomorphism_shomotopy_group_spi _ idp)⁻¹ᵍ,
+      apply shomotopy_group_isomorphism_of_pequiv, intro k,
+      apply ptrunc_pequiv, exact is_strunc_spi s₀ Y H k,
     end
 
 end atiyah_hirzebruch
+
+section serre
+  variables {X : Type} (F : X → Type) (Y : spectrum) (s₀ : ℤ) (H : is_strunc s₀ Y)
+
+  open option
+  definition add_point_over {X : Type} (F : X → Type) (x : option X) : Type* :=
+  (option.cases_on x (lift empty) F)₊
+
+  postfix `₊ₒ`:(max+1) := add_point_over
+
+  /- NOTE: we need unreduced cohomology, maybe also define aityah_hirzebruch for unreduced cohomology -/
+  include H
+  definition serre_convergence :
+    (λn s, opH^-n[(x : X₊), H^-s[F₊ₒ x, Y]]) ⟹ᵍ (λn, H^-n[(Σ(x : X), F x)₊, Y]) :=
+ -- (λn s, uopH^-n[(x : X), uH^-s[F x, Y]]) ⟹ᵍ (λn, uH^-n[Σ(x : X), F x, Y]) :=
+  proof
+  converges_to_g_isomorphism
+    (atiyah_hirzebruch_convergence (λx, sp_cotensor (F₊ₒ x) Y) s₀
+                                   (λx, is_strunc_sp_cotensor s₀ (F₊ₒ x) H))
+    begin
+      intro n s,
+      apply ordinary_parametrized_cohomology_isomorphism_right,
+      intro x,
+      exact (cohomology_isomorphism_shomotopy_group_sp_cotensor _ _ idp)⁻¹ᵍ,
+    end
+    begin
+      intro n, exact sorry
+--      refine parametrized_cohomology_isomorphism_shomotopy_group_spi _ idp ⬝g _,
+--      refine _ ⬝g (cohomology_isomorphism_shomotopy_group_sp_cotensor _ _ idp)⁻¹ᵍ,
+--      apply shomotopy_group_isomorphism_of_pequiv, intro k,
+    end
+ qed
+end serre
+
+/- TODO: πₛ[n] (strunc 0 (spi X Y)) ≃g H^n[X, λx, Y x] -/
+
+end spectrum
diff --git a/homotopy/spectrum.hlean b/homotopy/spectrum.hlean
index 67049e7..6207293 100644
--- a/homotopy/spectrum.hlean
+++ b/homotopy/spectrum.hlean
@@ -8,7 +8,7 @@ Authors: Michael Shulman, Floris van Doorn, Egbert Rijke, Stefano Piceghello, Yu
 import homotopy.LES_of_homotopy_groups .splice ..colim types.pointed2 .EM ..pointed_pi .smash_adjoint ..algebra.seq_colim .fwedge .pointed_cubes
 
 open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc_index pi group
-     seq_colim succ_str EM EM.ops function
+     seq_colim succ_str EM EM.ops function unit lift is_trunc
 
 /---------------------
   Basic definitions
@@ -253,6 +253,18 @@ namespace spectrum
   -- Equivalences of prespectra
   ------------------------------
 
+  definition spectrum_pequiv_of_nat {E F : spectrum} (e : Π(n : ℕ), E n ≃* F n) (n : ℤ) :
+    E n ≃* F n :=
+  begin
+    have Πn, E (n + 1) ≃* F (n + 1) → E n ≃* F n,
+    from λk f, equiv_glue E k ⬝e* loop_pequiv_loop f ⬝e* (equiv_glue F k)⁻¹ᵉ*,
+    induction n with n n,
+      exact e n,
+    induction n with n IH,
+    { exact this -[1+0] (e 0) },
+    { exact this -[1+succ n] IH }
+  end
+
   structure is_sequiv {N : succ_str} {E F : gen_prespectrum N} (f : E →ₛ F) : Type :=
   (to_linv : F →ₛ E)
   (is_retr : to_linv ∘ₛf ~ₛ sid E)
@@ -326,6 +338,13 @@ namespace spectrum
   definition psp_sphere : gen_prespectrum +ℕ :=
     psp_susp bool.pbool
 
+  ------------------------------
+  -- Contractible spectrum
+  ------------------------------
+
+  definition sunit.{u} [constructor] : spectrum.{u} :=
+  spectrum.MK (λn, plift punit) (λn, pequiv_of_is_contr _ _ _ _)
+
   /---------------------
     Homotopy groups
    ---------------------/
@@ -342,6 +361,14 @@ namespace spectrum
     πₛ[n] E →g πₛ[n] F :=
   π→g[2] (f (2 - n))
 
+  definition shomotopy_group_isomorphism_of_pequiv (n : ℤ) {E F : spectrum} (f : Πn, E n ≃* F n) :
+    πₛ[n] E ≃g πₛ[n] F :=
+  homotopy_group_isomorphism_of_pequiv 1 (f (2 - n))
+
+  definition shomotopy_group_isomorphism_of_pequiv_nat (n : ℕ) {E F : spectrum}
+    (f : Πn, E n ≃* F n) : πₛ[n] E ≃g πₛ[n] F :=
+  shomotopy_group_isomorphism_of_pequiv n (spectrum_pequiv_of_nat f)
+
   notation `πₛ→[`:95 n:0 `]`:0 := shomotopy_group_fun n
 
   -- what an awful name
@@ -405,7 +432,8 @@ namespace spectrum
     Fibers and long exact sequences
   -----------------------------------------/
 
-  definition sfiber {N : succ_str} {X Y : gen_spectrum N} (f : X →ₛ Y) : gen_spectrum N :=
+  definition sfiber [constructor] {N : succ_str} {X Y : gen_spectrum N} (f : X →ₛ Y) :
+    gen_spectrum N :=
     spectrum.MK (λn, pfiber (f n))
        (λn, (loop_pfiber (f (S n)))⁻¹ᵉ* ∘*ᵉ pfiber_pequiv_of_square _ _ (sglue_square f n))
 
@@ -728,6 +756,10 @@ spectrify_fun (smash_prespectrum_fun f g)
   definition EM_spectrum /-[constructor]-/ (G : AbGroup) : spectrum :=
   spectrum.Mk (K G) (λn, (loop_EM G n)⁻¹ᵉ*)
 
+  definition EM_spectrum_pequiv {G H : AbGroup} (e : G ≃g H) (n : ℤ) :
+    EM_spectrum G n ≃* EM_spectrum H n :=
+  spectrum_pequiv_of_nat (λk, EM_pequiv_EM k e) n
+
   /- Wedge of prespectra -/
 
 open fwedge
diff --git a/homotopy/strunc.hlean b/homotopy/strunc.hlean
index 0acf418..bbfec92 100644
--- a/homotopy/strunc.hlean
+++ b/homotopy/strunc.hlean
@@ -134,6 +134,10 @@ begin
     (maxm2_monotone (algebra.add_le_add_right H n))
 end
 
+definition is_strunc_pequiv_closed {k : ℤ} {E F : spectrum} (H : Πn, E n ≃* F n)
+  (H2 : is_strunc k E) : is_strunc k F :=
+λn, is_trunc_equiv_closed (maxm2 (k + n)) (H n)
+
 definition is_strunc_strunc (k : ℤ) (E : spectrum)
   : is_strunc k (strunc k E) :=
 λ n, is_trunc_trunc (maxm2 (k + n)) (E n)
@@ -255,7 +259,7 @@ section
 
 end
 
-definition is_strunc_spi (A : Type*) (k n : ℤ) (H : n ≤ k) (P : A → n-spectrum)
+definition is_strunc_spi_of_le {A : Type*} (k n : ℤ) (H : n ≤ k) (P : A → n-spectrum)
   : is_strunc k (spi A P) :=
 begin
   assert K : n ≤ -[1+ 0] + 1 + k,
@@ -266,4 +270,12 @@ begin
           (truncspectrum.struct (P a)))) }
 end
 
+definition is_strunc_spi {A : Type*} (n : ℤ) (P : A → spectrum) (H : Πa, is_strunc n (P a))
+  : is_strunc n (spi A P) :=
+is_strunc_spi_of_le n n !le.refl (λa, truncspectrum.mk (P a) (H a))
+
+definition is_strunc_sp_cotensor (n : ℤ) (A : Type*) {Y : spectrum} (H : is_strunc n Y)
+  : is_strunc n (sp_cotensor A Y) :=
+is_strunc_pequiv_closed (λn, !pppi_pequiv_ppmap) (is_strunc_spi n (λa, Y) (λa, H))
+
 end spectrum
diff --git a/move_to_lib.hlean b/move_to_lib.hlean
index dee29bd..9c2c4ee 100644
--- a/move_to_lib.hlean
+++ b/move_to_lib.hlean
@@ -227,6 +227,12 @@ namespace int
   definition sub_one_le (n : ℤ) : n - 1 ≤ n :=
   sub_nat_le n 1
 
+  definition le_add_nat (n : ℤ) (m : ℕ) : n ≤ n + m :=
+  le.intro rfl
+
+  definition le_add_one (n : ℤ) : n ≤ n + 1:=
+  le_add_nat n 1
+
 end int
 
 namespace pmap
@@ -236,6 +242,14 @@ namespace pmap
 
 end pmap
 
+namespace lift
+
+  definition is_trunc_plift [instance] [priority 1450] (A : Type*) (n : ℕ₋₂)
+    [H : is_trunc n A] : is_trunc n (plift A) :=
+  is_trunc_lift A n
+
+end lift
+
 namespace trunc
 
   -- TODO: redefine loopn_ptrunc_pequiv
diff --git a/pointed.hlean b/pointed.hlean
index 355125e..cd3c1dc 100644
--- a/pointed.hlean
+++ b/pointed.hlean
@@ -195,6 +195,9 @@ namespace pointed
   definition is_contr_loop (A : Type*) [is_set A] : is_contr (Ω A) :=
   is_contr.mk idp (λa, !is_prop.elim)
 
+  definition is_contr_punit [instance] : is_contr punit :=
+  is_contr_unit
+
   definition pequiv_of_is_contr (A B : Type*) (HA : is_contr A) (HB : is_contr B) : A ≃* B :=
   pequiv_punit_of_is_contr A _ ⬝e* (pequiv_punit_of_is_contr B _)⁻¹ᵉ*
 
diff --git a/pointed_pi.hlean b/pointed_pi.hlean
index 5eaf6ea..49943d7 100644
--- a/pointed_pi.hlean
+++ b/pointed_pi.hlean
@@ -399,7 +399,7 @@ namespace pointed
                 idpo)⁻¹ᵉ*
   qed
 
-  definition pmap_psigma {A B : Type*} (C : B → Type) (c : C pt) :
+  definition ppmap_psigma {A B : Type*} (C : B → Type) (c : C pt) :
     ppmap A (psigma_gen C c) ≃*
     psigma_gen (λ(f : ppmap A B), ppi_gen (C ∘ f) (transport C (respect_pt f)⁻¹ c))
                 (ppi_const _) :=
@@ -430,7 +430,7 @@ namespace pointed
                  refine !idp_con ⬝ _, symmetry, refine !ap_id ◾ !idp_con ⬝ _, apply con.right_inv
              end
       ... ≃* ppmap A (psigma_gen (λb, f b = pt) (respect_pt f)) :
-             by exact (pmap_psigma _ _)⁻¹ᵉ*
+             by exact (ppmap_psigma _ _)⁻¹ᵉ*
       ... ≃* ppmap A (pfiber f) : by exact pequiv_ppcompose_left !pfiber.sigma_char'⁻¹ᵉ*
 
 
@@ -460,6 +460,9 @@ namespace pointed
              by exact (ppi_psigma _ _)⁻¹ᵉ*
       ... ≃* Π*(a : A), pfiber (f a) : by exact ppi_pequiv_right (λa, !pfiber.sigma_char'⁻¹ᵉ*)
 
+  -- definition pppi_ppmap {A C : Type*} {B : A → Type*} :
+  --   ppmap (/- dependent smash of B -/) C ≃* Π*(a : A), ppmap (B a) C :=
+
 end pointed open pointed
 
 open is_trunc is_conn