diff --git a/homotopy/EM.hlean b/homotopy/EM.hlean
index 787a720..71fa19d 100644
--- a/homotopy/EM.hlean
+++ b/homotopy/EM.hlean
@@ -405,7 +405,7 @@ namespace EM
   begin
     cases n with n, { exact _ },
     cases Y with Y H1 H2, cases Y with Y y₀,
-    exact is_trunc_pmap_of_is_conn X n -1 (ptrunctype.mk Y _ y₀),
+    exact is_trunc_pmap_of_is_conn X n -1 _ (pointed.MK Y y₀) !le.refl H2,
   end
 
   open category functor nat_trans
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 3200777..24446cd 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 :=
@@ -309,14 +333,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)  :=
@@ -674,6 +700,56 @@ set_option pp.coercions true
     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
 
@@ -936,23 +1012,6 @@ set_option pp.coercions true
   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,
@@ -1082,6 +1141,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 f12c54a..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 :=
@@ -251,39 +251,33 @@ section
   variables (A : Type*) (n : ℤ) [H : is_conn (maxm2 n) A]
   include H
 
-  definition is_trunc_maxm2_ppi (k : ℤ) (P : A → (maxm2 (n+1+k))-Type*)
-    : is_trunc (maxm2 k) (Π*(a : A), P a) :=
+  definition is_trunc_maxm2_ppi (k l : ℤ) (H3 : l ≤ n+1+k) (P : A → Type*)
+    (H2 : Πa, is_trunc (maxm2 l) (P a)) : is_trunc (maxm2 k) (Π*(a : A), P a) :=
   is_trunc_maxm2_of_maxm1 (Π*(a : A), P a) k
-    (@is_trunc_ppi_of_is_conn A (maxm1m1 n)
-      (is_conn_maxm1_of_maxm2 A n H) (maxm1m1 k)
-      (λ a, ptrunctype.mk (P a) (is_trunc_of_le (P a) (maxm2_le n k)) pt))
+    (@is_trunc_ppi_of_is_conn A (maxm1m1 n) (is_conn_maxm1_of_maxm2 A n H) (maxm1m1 k) _
+      (le.trans (maxm2_monotone H3) (maxm2_le n k)) P H2)
 
-  definition is_strunc_spi_of_is_conn (k : ℤ) (P : A → (n+1+k)-spectrum)
-    : is_strunc k (spi A P) :=
+  definition is_strunc_spi_of_is_conn (k l : ℤ) (H3 : l ≤ n+1+k) (P : A → spectrum)
+    (H2 : Πa, is_strunc l (P a)) : is_strunc k (spi A P) :=
   begin
     intro m, unfold spi,
-    exact is_trunc_maxm2_ppi A n (k+m)
-      (λ a, ptrunctype.mk (P a m)
-       (is_trunc_maxm2_change_int (P a m) (add.assoc (n+1) k m)
-         (truncspectrum.struct (P a) m)) pt)
+    exact is_trunc_maxm2_ppi A n (k+m) _ (le.trans (add_le_add_right H3 _)
+            (le_of_eq (add.assoc (n+1) k m))) (λ a, P a m) (λa, H2 a m)
   end
 
 end
 
-definition is_strunc_spi_of_le {A : Type*} (k n : ℤ) (H : n ≤ k) (P : A → n-spectrum)
-  : is_strunc k (spi A P) :=
+definition is_strunc_spi_of_le {A : Type*} (k n : ℤ) (H : n ≤ k) (P : A → spectrum)
+  (H2 : Πa, is_strunc n (P a)) : is_strunc k (spi A P) :=
 begin
   assert K : n ≤ -[1+ 0] + 1 + k,
   { krewrite (int.zero_add k), exact H },
-  { exact @is_strunc_spi_of_is_conn A (-[1+ 0])
-    (is_conn.is_conn_minus_two A) k
-    (λ a, truncspectrum.mk (P a) (is_strunc_of_le (P a) K
-          (truncspectrum.struct (P a)))) }
+  { exact @is_strunc_spi_of_is_conn A (-[1+ 0]) (is_conn.is_conn_minus_two A) k _ K P H2 }
 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))
+is_strunc_spi_of_le n n !le.refl P H
 
 definition is_strunc_sp_cotensor (n : ℤ) (A : Type*) {Y : spectrum} (H : is_strunc n Y)
   : is_strunc n (sp_cotensor A Y) :=
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
diff --git a/pointed_pi.hlean b/pointed_pi.hlean
index ba5ab02..6a35cea 100644
--- a/pointed_pi.hlean
+++ b/pointed_pi.hlean
@@ -494,7 +494,7 @@ namespace is_conn
   variables (A : Type*) (n : ℕ₋₂) [H : is_conn (n.+1) A]
   include H
 
-  definition is_contr_ppi_match (P : A → (n.+1)-Type*)
+  definition is_contr_ppi_match (P : A → Type*) (H : Πa, is_trunc (n.+1) (P a))
     : is_contr (Π*(a : A), P a) :=
   begin
     apply is_contr.mk pt,
@@ -504,44 +504,46 @@ namespace is_conn
     { krewrite (is_conn.elim_β n), apply con.left_inv }
   end
 
-  definition is_trunc_ppi_of_is_conn (k : ℕ₋₂) (P : A → (n.+1+2+k)-Type*)
-    : is_trunc k.+1 (Π*(a : A), P a) :=
+  -- definition is_trunc_ppi_of_is_conn (k : ℕ₋₂) (P : A → Type*)
+  --   : is_trunc k.+1 (Π*(a : A), P a) :=
+
+  definition is_trunc_ppi_of_is_conn (k l : ℕ₋₂) (H2 : l ≤ n.+1+2+k)
+    (P : A → Type*) (H3 : Πa, is_trunc l (P a)) :
+    is_trunc k.+1 (Π*(a : A), P a) :=
   begin
-    induction k with k IH,
+    have H4 : Πa, is_trunc (n.+1+2+k) (P a), from λa, is_trunc_of_le (P a) H2,
+    clear H2 H3, revert P H4,
+    induction k with k IH: intro P H4,
     { apply is_prop_of_imp_is_contr, intro f,
-      apply is_contr_ppi_match },
+      apply is_contr_ppi_match A n P H4 },
     { apply is_trunc_succ_of_is_trunc_loop
         (trunc_index.succ_le_succ (trunc_index.minus_two_le k)),
       intro f,
-      apply @is_trunc_equiv_closed_rev _ _ k.+1
-        (ppi_loop_equiv f),
+      apply @is_trunc_equiv_closed_rev _ _ k.+1 (ppi_loop_equiv f),
       apply IH, intro a,
-      apply ptrunctype.mk (Ω (pType.mk (P a) (f a))),
-      { apply is_trunc_loop, exact is_trunc_ptrunctype (P a) },
-      { exact pt } }
+      apply is_trunc_loop, apply H4 }
   end
 
-  definition is_trunc_pmap_of_is_conn (k : ℕ₋₂) (B : (n.+1+2+k)-Type*)
-    : is_trunc k.+1 (A →* B) :=
+
+  definition is_trunc_pmap_of_is_conn (k l : ℕ₋₂) (B : Type*) (H2 : l ≤ n.+1+2+k)
+    (H3 : is_trunc l B) : is_trunc k.+1 (A →* B) :=
   @is_trunc_equiv_closed _ _ k.+1 (ppi_equiv_pmap A B)
-    (is_trunc_ppi_of_is_conn A n k (λ a, B))
+    (is_trunc_ppi_of_is_conn A n k l H2 (λ a, B) _)
 
   end
 
   -- this is probably much easier to prove directly
-  definition is_trunc_ppi (A : Type*) (n k : ℕ₋₂) (H : n ≤ k) (P : A → n-Type*)
-    : is_trunc k (Π*(a : A), P a) :=
+  definition is_trunc_ppi (A : Type*) (n k : ℕ₋₂) (H : n ≤ k) (P : A → Type*)
+    (H2 : Πa, is_trunc n (P a)) : is_trunc k (Π*(a : A), P a) :=
   begin
     cases k with k,
-    { apply trunc.is_contr_of_merely_prop,
-      { exact @is_trunc_ppi_of_is_conn A -2 (is_conn_minus_one A (tr pt)) -2
-          (λ a, ptrunctype.mk (P a) (is_trunc_of_le (P a)
-                  (trunc_index.le.step H)) pt) },
+    { apply is_contr_of_merely_prop,
+      { exact @is_trunc_ppi_of_is_conn A -2 (is_conn_minus_one A (tr pt)) -2 _
+                (trunc_index.le.step H) P H2 },
       { exact tr pt } },
     { assert K : n ≤ -1 +2+ k,
       { rewrite (trunc_index.add_plus_two_comm -1 k), exact H },
-      { exact @is_trunc_ppi_of_is_conn A -2 (is_conn_minus_one A (tr pt)) k
-          (λ a, ptrunctype.mk (P a) (is_trunc_of_le (P a) K) pt) } }
+      { exact @is_trunc_ppi_of_is_conn A -2 (is_conn_minus_one A (tr pt)) k _ K P H2 } }
   end
 
 end is_conn