diff --git a/homotopy/serre.hlean b/homotopy/serre.hlean
index ad82b65..cef85d5 100644
--- a/homotopy/serre.hlean
+++ b/homotopy/serre.hlean
@@ -8,7 +8,7 @@ set_option pp.binder_types true
 
 namespace pointed
 definition postnikov_map [constructor] (A : Type*) (n : ℕ₋₂) : ptrunc (n.+1) A →* ptrunc n A :=
-ptrunc.elim (n.+1) !ptr
+ptrunc.elim (n.+1) (ptr n A)
 
 definition ptrunc_functor_postnikov_map {A B : Type*} (n : ℕ₋₂) (f : A →* B) :
   ptrunc_functor n f ∘* postnikov_map A n ~* ptrunc.elim (n.+1) (!ptr ∘* f) :=
@@ -68,39 +68,95 @@ this⁻¹ᵛ*
 end pointed open pointed
 
 namespace spectrum
-
+/- begin move -/
 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
 
+definition ptrunc_maxm2_pred {n m : ℤ} (A : Type*) (p : n - 1 = m) :
+  ptrunc (maxm2 m) A ≃* ptrunc (trunc_index.pred (maxm2 n)) A :=
+begin
+  cases n with n, cases n with n, apply pequiv_of_is_contr,
+        induction p, apply is_trunc_trunc,
+      apply is_contr_ptrunc_minus_one,
+    exact ptrunc_change_index (ap maxm2 (p⁻¹ ⬝ !add_sub_cancel)) A,
+  exact ptrunc_change_index (ap maxm2 p⁻¹) A
+end
+
+definition ptrunc_maxm2_pred_nat {n : ℕ} {m l : ℤ} (A : Type*)
+  (p : nat.succ n = l) (q : pred l = m) (r : maxm2 m = trunc_index.pred (maxm2 (nat.succ n))) :
+  @ptrunc_maxm2_pred (nat.succ n) m A (ap pred p ⬝ q) ~* ptrunc_change_index r A :=
+begin
+  have ap maxm2 ((ap pred p ⬝ q)⁻¹ ⬝ add_sub_cancel n 1) = r, from !is_set.elim,
+  induction this, reflexivity
+end
+
+definition EM_type_pequiv_EM (A : spectrum) (n k : ℤ) (l : ℕ) (p : n + k = l) :
+  EM_type (A k) l ≃* EM (πₛ[n] A) l :=
+begin
+  symmetry,
+  cases l with l,
+  { exact shomotopy_group_pequiv_homotopy_group A p },
+  { cases l with l,
+    { apply EM1_pequiv_EM1, exact shomotopy_group_isomorphism_homotopy_group A p },
+    { apply EMadd1_pequiv_EMadd1 (l+1), exact shomotopy_group_isomorphism_homotopy_group A p }}
+end
+/- end move -/
+
 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)
 
-/-
-  we could try to prove that postnikov_smap is homotopic to postnikov_map, although the types
-  are different enough, that even stating it will be quite annoying
--/
+definition postnikov_map_pred (A : Type*) (n : ℕ₋₂) :
+  ptrunc n A →* ptrunc (trunc_index.pred n) A :=
+begin cases n with n, exact !pid, exact postnikov_map A n end
+
+definition pfiber_postnikov_map_pred (A : Type*) (n : ℕ) :
+  pfiber (postnikov_map_pred A n) ≃* EM_type A n :=
+begin
+  cases n with n,
+    apply pfiber_pequiv_of_is_contr, apply is_contr_ptrunc_minus_one,
+  exact pfiber_postnikov_map A n
+end
+
+definition pfiber_postnikov_map_pred' (A : spectrum) (n k l : ℤ) (p : n + k = l) :
+  pfiber (postnikov_map_pred (A k) (maxm2 l)) ≃* EM_spectrum (πₛ[n] A) l :=
+begin
+  cases l with l l,
+  { refine pfiber_postnikov_map_pred (A k) l ⬝e* _,
+    exact EM_type_pequiv_EM A n k l p },
+  { apply pequiv_of_is_contr, apply is_contr_pfiber_pid,
+    apply is_contr_EM_spectrum_neg }
+end
+
+definition psquare_postnikov_map_ptrunc_elim (A : Type*) {n k l : ℕ₋₂} (H : is_trunc n (ptrunc k A))
+  (p : n = l.+1) (q : k = l) :
+  psquare (ptrunc.elim n (ptr k A)) (postnikov_map A l)
+          (ptrunc_change_index p A) (ptrunc_change_index q A) :=
+begin
+  induction q, cases p,
+  refine _ ⬝pv* pvrfl,
+  apply ptrunc_elim_phomotopy2,
+  reflexivity
+end
+
+definition postnikov_smap_postnikov_map (A : spectrum) (n k l : ℤ) (p : n + k = l) :
+  psquare (postnikov_smap A n k) (postnikov_map_pred (A k) (maxm2 l))
+    (ptrunc_maxm2_change_int p (A k)) (ptrunc_maxm2_pred (A k) (ap pred p⁻¹ ⬝ add.right_comm n k (- 1))) :=
+begin
+  cases l with l,
+  { cases l with l, apply phomotopy_of_is_contr_cod, apply is_contr_ptrunc_minus_one,
+    refine psquare_postnikov_map_ptrunc_elim (A k) _ _ _ ⬝hp* _,
+    exact ap maxm2 (add.right_comm n (- 1) k ⬝ ap pred p ⬝ !pred_succ),
+    apply ptrunc_maxm2_pred_nat },
+  { apply phomotopy_of_is_contr_cod, apply is_trunc_trunc }
+end
 
 definition pfiber_postnikov_smap (A : spectrum) (n : ℤ) (k : ℤ) :
-  sfiber (postnikov_smap A n) k ≃* EM_spectrum (πₛ[n] A) k :=
-begin
-  exact sorry
-/-  symmetry, apply spectrum_pequiv_of_nat_succ_succ, clear k, intro k,
-  apply EMadd1_pequiv k,
-  { exact sorry
-    -- refine _ ⬝g shomotopy_group_strunc n A,
-    -- exact chain_complex.LES_isomorphism_of_trivial_cod _ _
-    --   (trivial_homotopy_group_of_is_trunc _ (self_lt_succ n))
-    --   (trivial_homotopy_group_of_is_trunc _ (le_succ _))
-},
-  { exact sorry --apply is_conn_fun_trunc_elim,  apply is_conn_fun_tr
-    },
-  { -- have is_trunc (n+1) (ptrunc n.+1 A), from !is_trunc_trunc,
-    -- have is_trunc ((n+1).+1) (ptrunc n A), by do 2 apply is_trunc_succ, apply is_trunc_trunc,
-    -- apply is_trunc_pfiber
-    exact sorry
-    }-/
-end
+  sfiber (postnikov_smap A n) k ≃* EM_spectrum (πₛ[n] A) (n + k) :=
+proof
+pfiber_pequiv_of_square _ _ (postnikov_smap_postnikov_map A n k (n + k) idp) ⬝e*
+pfiber_postnikov_map_pred' A n k _ idp
+qed
 
 section atiyah_hirzebruch
   parameters {X : Type*} (Y : X → spectrum) (s₀ : ℤ) (H : Πx, is_strunc s₀ (Y x))
@@ -141,10 +197,18 @@ section atiyah_hirzebruch
     (λ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 n : ℤ) :
-    EM_spectrum (πₛ[n] (spi X Y)) k ≃* spi X (λx, EM_spectrum (πₛ[n] (Y x))) k :=
-  sorry
+  lemma spi_EM_spectrum (n : ℤ) : Π(k : ℤ),
+    EM_spectrum (πₛ[n] (spi X Y)) (n + k) ≃* spi X (λx, EM_spectrum (πₛ[n] (Y x))) k :=
+  begin
+    exact sorry
+    -- apply spectrum_pequiv_of_nat_add 2, intro k,
+    -- fapply EMadd1_pequiv (k+1),
+    -- { exact sorry },
+    -- { exact sorry },
+    -- { apply is_trunc_ppi, rotate 1, intro x,  },
+  end
 
+set_option formatter.hide_full_terms false
   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'
diff --git a/homotopy/spectrum.hlean b/homotopy/spectrum.hlean
index 116214c..1394a5b 100644
--- a/homotopy/spectrum.hlean
+++ b/homotopy/spectrum.hlean
@@ -59,6 +59,30 @@ namespace spectrum
     exact add.assoc n 1 1
   end
 
+  definition gluen {N : succ_str} (X : gen_prespectrum N) (n : N) (k : ℕ)
+    : X n →* Ω[k] (X (n +' k)) :=
+  by induction k with k f; reflexivity; exact !loopn_succ_in⁻¹ᵉ* ∘* Ω→[k] (glue X (n +' k)) ∘* f
+
+  -- note: the forward map is (currently) not definitionally equal to gluen. Is that a problem?
+  definition equiv_gluen {N : succ_str} (X : gen_spectrum N) (n : N) (k : ℕ)
+    : X n ≃* Ω[k] (X (n +' k)) :=
+  by induction k with k f; reflexivity; exact f ⬝e* (loopn_pequiv_loopn k (equiv_glue X (n +' k))
+                                                ⬝e* !loopn_succ_in⁻¹ᵉ*)
+
+  definition equiv_gluen_inv_succ {N : succ_str} (X : gen_spectrum N) (n : N) (k : ℕ) :
+    (equiv_gluen X n (k+1))⁻¹ᵉ* ~*
+    (equiv_gluen X n k)⁻¹ᵉ* ∘* Ω→[k] (equiv_glue X (n +' k))⁻¹ᵉ* ∘* !loopn_succ_in :=
+  begin
+    refine !trans_pinv ⬝* pwhisker_left _ _, refine !trans_pinv ⬝* _, refine pwhisker_left _ !pinv_pinv
+  end
+
+  definition succ_str_add_eq_int_add (n : ℤ) (m : ℕ) : @succ_str.add sint n m = n + m :=
+  begin
+    induction m with m IH,
+    { symmetry, exact add_zero n },
+    { exact ap int.succ IH ⬝ add.assoc n m 1 }
+  end
+
   -- a square when we compose glue with transporting over a path in N
   definition glue_ptransport {N : succ_str} (X : gen_prespectrum N) {n n' : N} (p : n = n') :
     glue X n' ∘* ptransport X p ~* Ω→ (ptransport X (ap S p)) ∘* glue X n :=
@@ -267,14 +291,16 @@ namespace spectrum
     { exact spectrum_pequiv_of_pequiv_succ -[1+succ n] IH }
   end
 
-  -- definition spectrum_pequiv_of_nat_add {E F : spectrum} (m : ℕ)
-  --   (e : Π(n : ℕ), E (n + m) ≃* F (n + m)) : Π(n : ℤ), E n ≃* F n :=
-  -- begin
-  --   apply spectrum_pequiv_of_nat,
-  --   refine nat.rec_down _ m e _,
-  --   intro n f m, cases m with m,
-
-  -- end
+  definition spectrum_pequiv_of_nat_add {E F : spectrum} (m : ℕ)
+    (e : Π(n : ℕ), E (n + m) ≃* F (n + m)) : Π(n : ℤ), E n ≃* F n :=
+  begin
+    apply spectrum_pequiv_of_nat,
+    refine nat.rec_down _ m e _,
+    intro n f k, cases k with k,
+    exact spectrum_pequiv_of_pequiv_succ _ (f 0),
+    exact pequiv_ap E (ap of_nat (succ_add k n)) ⬝e* f k ⬝e*
+          pequiv_ap F (ap of_nat (succ_add k n))⁻¹
+  end
 
   definition is_contr_spectrum_of_nat {E : spectrum} (e : Π(n : ℕ), is_contr (E n)) (n : ℤ) :
     is_contr (E n)  :=
@@ -496,6 +522,56 @@ namespace spectrum
     refine !sglue_square ⬝v* ap1_psquare !pequiv_of_eq_commute
   end
 
+  definition homotopy_group_spectrum_irrel_one {n m : ℤ} {k : ℕ} (E : spectrum) (p : n + 1 = m + k)
+    [Hk : is_succ k] : πg[k] (E n) ≃g π₁ (E m) :=
+  begin
+    induction Hk with k,
+    change π₁ (Ω[k] (E n)) ≃g π₁ (E m),
+    apply homotopy_group_isomorphism_of_pequiv 0,
+    symmetry,
+    have m + k = n, from (pred_succ (m + k))⁻¹ ⬝ ap pred (add.assoc m k 1 ⬝ p⁻¹) ⬝ pred_succ n,
+    induction (succ_str_add_eq_int_add m k ⬝ this),
+    exact equiv_gluen E m k
+  end
+
+  definition homotopy_group_spectrum_irrel {n m : ℤ} {l k : ℕ} (E : spectrum) (p : n + l = m + k)
+    [Hk : is_succ k] [Hl : is_succ l] : πg[k] (E n) ≃g πg[l] (E m) :=
+  have Πa b c : ℤ, a + (b + c) = c + (b + a), from λa b c,
+  !add.assoc⁻¹ ⬝ add.comm (a + b) c ⬝ ap (λx, c + x) (add.comm a b),
+  have n + 1 = m + 1 - l + k, from
+  ap succ (add_sub_cancel n l)⁻¹ ⬝ !add.assoc ⬝ ap (λx, x + (-l + 1)) p ⬝ !add.assoc ⬝
+  ap (λx, m + x) (this k (-l) 1) ⬝ !add.assoc⁻¹ ⬝ !add.assoc⁻¹,
+  homotopy_group_spectrum_irrel_one E this ⬝g
+  (homotopy_group_spectrum_irrel_one E (sub_add_cancel (m+1) l)⁻¹)⁻¹ᵍ
+
+  definition shomotopy_group_isomorphism_homotopy_group {n m : ℤ} {l : ℕ} (E : spectrum) (p : n + m = l)
+    [H : is_succ l] : πₛ[n] E ≃g πg[l] (E m) :=
+  have 2 - n + l = m + 2, from
+  ap (λx, 2 - n + x) p⁻¹ ⬝ !add.assoc⁻¹ ⬝ ap (λx, x + m) (sub_add_cancel 2 n) ⬝ add.comm 2 m,
+  homotopy_group_spectrum_irrel E this
+
+  definition shomotopy_group_pequiv_homotopy_group_ab {n m : ℤ} {l : ℕ} (E : spectrum) (p : n + m = l)
+    [H : is_at_least_two l] : πₛ[n] E ≃g πag[l] (E m) :=
+  begin
+    induction H with l,
+    exact shomotopy_group_isomorphism_homotopy_group E p
+  end
+
+  definition shomotopy_group_pequiv_homotopy_group {n m : ℤ} {l : ℕ} (E : spectrum) (p : n + m = l) :
+    πₛ[n] E ≃* π[l] (E m) :=
+  begin
+    cases l with l,
+    { apply ptrunc_pequiv_ptrunc, symmetry,
+      change E m ≃* Ω (Ω (E (2 - n))),
+      refine !equiv_glue ⬝e* loop_pequiv_loop _,
+      refine !equiv_glue ⬝e* loop_pequiv_loop _,
+      apply pequiv_ap E,
+      have -n = m, from neg_eq_of_add_eq_zero p,
+      induction this,
+      rexact add.assoc (-n) 1 1 ⬝ add.comm (-n) 2 },
+    { exact pequiv_of_isomorphism (shomotopy_group_isomorphism_homotopy_group E p) }
+  end
+
   section
   open chain_complex prod fin group
 
@@ -690,23 +766,6 @@ namespace spectrum
   definition spectrify [constructor] {N : succ_str} (X : gen_prespectrum N) : gen_spectrum N :=
   spectrum.MK (spectrify_type X) (spectrify_pequiv X)
 
-  definition gluen {N : succ_str} (X : gen_prespectrum N) (n : N) (k : ℕ)
-    : X n →* Ω[k] (X (n +' k)) :=
-  by induction k with k f; reflexivity; exact !loopn_succ_in⁻¹ᵉ* ∘* Ω→[k] (glue X (n +' k)) ∘* f
-
-  -- note: the forward map is (currently) not definitionally equal to gluen. Is that a problem?
-  definition equiv_gluen {N : succ_str} (X : gen_spectrum N) (n : N) (k : ℕ)
-    : X n ≃* Ω[k] (X (n +' k)) :=
-  by induction k with k f; reflexivity; exact f ⬝e* (loopn_pequiv_loopn k (equiv_glue X (n +' k))
-                                                ⬝e* !loopn_succ_in⁻¹ᵉ*)
-
-  definition equiv_gluen_inv_succ {N : succ_str} (X : gen_spectrum N) (n : N) (k : ℕ) :
-    (equiv_gluen X n (k+1))⁻¹ᵉ* ~*
-    (equiv_gluen X n k)⁻¹ᵉ* ∘* Ω→[k] (equiv_glue X (n +' k))⁻¹ᵉ* ∘* !loopn_succ_in :=
-  begin
-    refine !trans_pinv ⬝* pwhisker_left _ _, refine !trans_pinv ⬝* _, refine pwhisker_left _ !pinv_pinv
-  end
-
   definition spectrify_map {N : succ_str} {X : gen_prespectrum N} : X →ₛ spectrify X :=
   begin
     fapply smap.mk,
@@ -836,6 +895,13 @@ spectrify_fun (smash_prespectrum_fun f g)
     (is_contr_spectrum_of_nat (λk, is_contr_EM k !is_trunc_lift) n)
     !is_trunc_lift
 
+  definition is_contr_EM_spectrum_neg (G : AbGroup) (n : ℕ) : is_contr (EM_spectrum G (-[1+n])) :=
+  begin
+    induction n with n IH,
+    { apply is_contr_loop, exact is_trunc_EM G 0 },
+    { apply is_contr_loop_of_is_contr, exact IH }
+  end
+
   /- Wedge of prespectra -/
 
 open fwedge
diff --git a/homotopy/strunc.hlean b/homotopy/strunc.hlean
index db4f67c..264dfc7 100644
--- a/homotopy/strunc.hlean
+++ b/homotopy/strunc.hlean
@@ -40,7 +40,7 @@ namespace spectrum
 
 definition ptrunc_maxm2_change_int {k l : ℤ} (p : k = l) (X : Type*)
   : ptrunc (maxm2 k) X ≃* ptrunc (maxm2 l) X :=
-pequiv_ap (λ n, ptrunc (maxm2 n) X) p
+ptrunc_change_index (ap maxm2 p) X
 
 definition is_trunc_maxm2_change_int {k l : ℤ} (X : pType) (p : k = l)
   : is_trunc (maxm2 k) X → is_trunc (maxm2 l) X :=
diff --git a/move_to_lib.hlean b/move_to_lib.hlean
index eb63d24..df2bfe7 100644
--- a/move_to_lib.hlean
+++ b/move_to_lib.hlean
@@ -232,7 +232,7 @@ namespace int
   definition le_add_one (n : ℤ) : n ≤ n + 1:=
   le_add_nat n 1
 
-end int
+end int open int
 
 namespace pmap
 
@@ -250,6 +250,15 @@ namespace lift
 end lift
 
 namespace trunc
+  open trunc_index
+  definition trunc_index_equiv_nat [constructor] : ℕ₋₂ ≃ ℕ :=
+  equiv.MK add_two sub_two add_two_sub_two sub_two_add_two
+
+  definition is_set_trunc_index [instance] : is_set ℕ₋₂ :=
+  is_trunc_equiv_closed_rev 0 trunc_index_equiv_nat
+
+  definition is_contr_ptrunc_minus_one (A : Type*) : is_contr (ptrunc -1 A) :=
+  is_contr_of_inhabited_prop pt
 
   -- TODO: redefine loopn_ptrunc_pequiv
   definition apn_ptrunc_functor (n : ℕ₋₂) (k : ℕ) {A B : Type*} (f : A →* B) :
@@ -320,6 +329,9 @@ namespace trunc
   have is_trunc k (ptrunc l X), from is_trunc_of_le _ p,
   ptrunc.elim _ (ptr l X)
 
+  definition trunc_index.pred [unfold 1] (n : ℕ₋₂) : ℕ₋₂ :=
+  begin cases n with n, exact -2, exact n end
+
 end trunc
 
 namespace is_trunc
@@ -419,6 +431,13 @@ namespace group
 
 end group open group
 
+namespace fiber
+
+  definition is_contr_pfiber_pid (A : Type*) : is_contr (pfiber (pid A)) :=
+  is_contr.mk pt begin intro x, induction x with a p, esimp at p, cases p, reflexivity end
+
+end fiber
+
 namespace function
   variables {A B : Type} {f f' : A → B}
   open is_conn sigma.ops
diff --git a/pointed.hlean b/pointed.hlean
index 3412b51..cb6bbac 100644
--- a/pointed.hlean
+++ b/pointed.hlean
@@ -2,7 +2,7 @@
 
 -- Author: Floris van Doorn
 
-import types.pointed2
+import types.pointed2 .move_to_lib
 
 open pointed eq equiv function is_equiv unit is_trunc trunc nat algebra sigma group
 
@@ -220,5 +220,4 @@ namespace pointed
     begin rewrite [▸*, is_prop_elim_self, +ap_idp, idp_con, con_idp, inv_con_cancel_right] end
 
 
-
 end pointed