diff --git a/homotopy/EM.hlean b/homotopy/EM.hlean
index 7080a30..ccba43e 100644
--- a/homotopy/EM.hlean
+++ b/homotopy/EM.hlean
@@ -4,6 +4,8 @@ import homotopy.EM algebra.category.functor.equivalence types.pointed2 ..pointed
 
 open eq equiv is_equiv algebra group nat pointed EM.ops is_trunc trunc susp function is_conn
 
+/- TODO: try to fix up this file -/
+
 namespace EM
 
   definition EMadd1_functor_succ [unfold_full] {G H : AbGroup} (φ : G →g H) (n : ℕ) :
@@ -300,6 +302,24 @@ namespace EM
   EMadd1_pequiv_succ_natural f n !isomorphism.refl !isomorphism.refl (π→g[n+2] f)
     proof λa, idp qed
 
+  /- The Eilenberg-MacLane space K(G,n) with the same homotopy group as X on level n -/
+  definition EM_type (X : Type*) : ℕ → Type*
+  | 0     := ptrunc 0 X
+  | 1     := EM1 (π₁ X)
+  | (n+2) := EMadd1 (πag[n+2] X) (n+1)
+
+  definition EM_type_pequiv.{u} {X Y : pType.{u}} (n : ℕ) [Hn : is_succ n] (e : πg[n] Y ≃g πg[n] X)
+    [H1 : is_conn (n.-1) X] [H2 : is_trunc n X] : EM_type Y n ≃* X :=
+  begin
+    induction Hn with n, cases n with n,
+    { have is_conn 0 X, from H1,
+      have is_trunc 1 X, from H2,
+      exact EM1_pequiv e },
+    { have is_conn (n+1) X, from H1,
+      have is_trunc ((n+1).+1) X, from H2,
+      exact EMadd1_pequiv (n+1) e⁻¹ᵍ }
+  end
+
   -- definition EM1_functor_equiv' (X Y : Type*) [H1 : is_conn 0 X] [H2 : is_trunc 1 X]
   --   [H3 : is_conn 0 Y] [H4 : is_trunc 1 Y] : (X →* Y) ≃ (π₁ X →g π₁ Y) :=
   -- begin
@@ -387,7 +407,8 @@ namespace EM
     exact is_trunc_pmap_of_is_conn X n -1 (ptrunctype.mk Y _ y₀),
   end
 
-  open category
+  open category functor nat_trans
+
   definition precategory_ptruncconntype'.{u} [constructor] (n : ℕ₋₂) :
     precategory.{u+1 u} (ptruncconntype' n) :=
   begin
@@ -412,8 +433,6 @@ namespace EM
   definition tEM [constructor] (G : AbGroup) (n : ℕ) : ptruncconntype' (n.-1) :=
   ptruncconntype'.mk (EM G n) _ !is_trunc_EM
 
-  open functor
-
   definition EM1_cfunctor : Grp ⇒ cType*[0] :=
   functor.mk
     (λG, tEM1 G)
@@ -442,7 +461,6 @@ namespace EM
     begin intro, apply homomorphism_eq, exact to_homotopy !homotopy_group_functor_pid end
     begin intros, apply homomorphism_eq, exact to_homotopy !homotopy_group_functor_compose end
 
-  open nat_trans category
 
   definition is_equivalence_EM1_cfunctor.{u} : is_equivalence EM1_cfunctor.{u} :=
   begin
@@ -500,23 +518,8 @@ namespace EM
   end category
 
   /- move -/
-  -- switch arguments in homotopy_group_trunc_of_le
-  lemma ghomotopy_group_trunc_of_le (k n : ℕ) (A : Type*) [Hk : is_succ k] (H : k ≤[ℕ] n)
-    : πg[k] (ptrunc n A) ≃g πg[k] A :=
-  begin
-    exact sorry
-  end
-
-  lemma homotopy_group_isomorphism_of_ptrunc_pequiv {A B : Type*}
-    (n k : ℕ) (H : n+1 ≤[ℕ] k) (f : ptrunc k A ≃* ptrunc k B) : πg[n+1] A ≃g πg[n+1] B :=
-  (ghomotopy_group_trunc_of_le _ k A H)⁻¹ᵍ ⬝g
-  homotopy_group_isomorphism_of_pequiv n f ⬝g
-  ghomotopy_group_trunc_of_le _ k B H
 
   open trunc_index
-  lemma minus_two_add_plus_two (n : ℕ₋₂) : -2+2+n = n :=
-  by induction n with n p; reflexivity; exact ap succ p
-
   definition is_trunc_succ_of_is_trunc_loop (n : ℕ₋₂) (A : Type*) (H : is_trunc (n.+1) (Ω A))
     (H2 : is_conn 0 A) : is_trunc (n.+2) A :=
   begin
@@ -553,69 +556,37 @@ namespace EM
   end
 
   definition EM1_pequiv_EM1 {G H : Group} (φ : G ≃g H) : EM1 G ≃* EM1 H :=
-  sorry
+  pequiv.MK (EM1_functor φ) (EM1_functor φ⁻¹ᵍ)
+    abstract (EM1_functor_gcompose φ⁻¹ᵍ φ)⁻¹* ⬝* EM1_functor_phomotopy proof left_inv φ qed ⬝*
+             EM1_functor_gid G end
+    abstract (EM1_functor_gcompose φ φ⁻¹ᵍ)⁻¹* ⬝* EM1_functor_phomotopy proof right_inv φ qed ⬝*
+             EM1_functor_gid H end
 
   definition EMadd1_pequiv_EMadd1 (n : ℕ) {G H : AbGroup} (φ : G ≃g H) : EMadd1 G n ≃* EMadd1 H n :=
-  sorry
+  pequiv.MK (EMadd1_functor φ n) (EMadd1_functor φ⁻¹ᵍ n)
+    abstract (EMadd1_functor_gcompose φ⁻¹ᵍ φ n)⁻¹* ⬝* EMadd1_functor_phomotopy proof left_inv φ qed n ⬝*
+             EMadd1_functor_gid G n end
+    abstract (EMadd1_functor_gcompose φ φ⁻¹ᵍ n)⁻¹* ⬝* EMadd1_functor_phomotopy proof right_inv φ qed n ⬝*
+             EMadd1_functor_gid H n end
 
   /- Eilenberg MacLane spaces are the fibers of the Postnikov system of a type -/
 
   definition postnikov_map [constructor] (A : Type*) (n : ℕ₋₂) : ptrunc (n.+1) A →* ptrunc n A :=
   ptrunc.elim (n.+1) !ptr
 
-  open fiber EM.ops
+  open fiber
 
-  -- move
-
-  definition pgroup_of_Group (X : Group) : pgroup X :=
-  pgroup_of_group _ idp
-
-  -- open prod chain_complex succ_str fin
-  -- definition isomorphism_of_trivial_LES {A B : Type*} (f : A →* B) (n : ℕ)
-  --   (k : fin (nat.succ 2)) (HX1 : is_contr (homotopy_groups f (n+1, k)))
-  --   (HX2 : is_contr (homotopy_groups f (n+2, k))) :
-  --   Group_LES_of_homotopy_groups f (@S +3ℕ (S (n, k))) ≃g Group_LES_of_homotopy_groups f (S (n, k)) :=
-  -- begin
-  --   induction k with k Hk,
-  --   cases k with k, rotate 1, cases k with k, rotate 1, cases k with k, rotate 1,
-  --   exfalso, apply lt_le_antisymm Hk, apply le_add_left,
-  --   all_goals exact let k := fin.mk _ Hk in let x : +3ℕ := (n, k) in let S : +3ℕ → +3ℕ := succ_str.S in
-  --     let z :=
-  --     @is_equiv_of_trivial _
-  --       (LES_of_homotopy_groups f) _
-  --       (is_exact_LES_of_homotopy_groups f (n+1, k))
-  --       (is_exact_LES_of_homotopy_groups f (S (n+1, k)))
-  --       HX1 HX2
-  --       (pgroup_of_Group (Group_LES_of_homotopy_groups f (S x)))
-  --       (pgroup_of_Group (Group_LES_of_homotopy_groups f (S (S x))))
-  --       (homomorphism.struct (homomorphism_LES_of_homotopy_groups_fun f (S x))) in
-  --     isomorphism.mk (homomorphism_LES_of_homotopy_groups_fun f _) z
-  -- end
-
-
-  definition pfiber_postnikov_map_zero (A : Type*) :
-    pfiber (postnikov_map A 0) ≃* EM1 (πg[1] A) :=
+  definition pfiber_postnikov_map (A : Type*) (n : ℕ) : pfiber (postnikov_map A n) ≃* EM_type A (n+1) :=
   begin
-    symmetry, apply EM1_pequiv,
-    { symmetry, refine _ ⬝g ghomotopy_group_ptrunc 1 A,
+    symmetry, apply EM_type_pequiv,
+    { symmetry, refine _ ⬝g ghomotopy_group_ptrunc (n+1) A,
       exact chain_complex.LES_isomorphism_of_trivial_cod _ _
-        (trivial_homotopy_group_of_is_trunc _ !zero_lt_one)
-        (trivial_homotopy_group_of_is_trunc _ (zero_lt_succ 1)) },
-    { apply @is_conn_fun_trunc_elim, apply is_conn_fun_tr },
-    { apply is_trunc_pfiber }
-  end
-
-  definition pfiber_postnikov_map_succ (A : Type*) (n : ℕ) :
-    pfiber (postnikov_map A (n+1)) ≃* EMadd1 (πag[n+2] A) (n+1) :=
-  begin
-    symmetry, apply EMadd1_pequiv,
-    { refine _ ⬝g ghomotopy_group_ptrunc (n+2) A,
-      exact chain_complex.LES_isomorphism_of_trivial_cod _ _
-        (trivial_homotopy_group_of_is_trunc _ (self_lt_succ (n+1)))
+        (trivial_homotopy_group_of_is_trunc _ (self_lt_succ n))
         (trivial_homotopy_group_of_is_trunc _ (le_succ _)) },
     { apply is_conn_fun_trunc_elim,  apply is_conn_fun_tr },
-    { apply is_trunc_pfiber }
+    { 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 }
   end
 
-
 end EM
diff --git a/move_to_lib.hlean b/move_to_lib.hlean
index 5e0fe4b..f3a6464 100644
--- a/move_to_lib.hlean
+++ b/move_to_lib.hlean
@@ -2,8 +2,8 @@
 
 import homotopy.sphere2 homotopy.cofiber homotopy.wedge hit.prop_trunc hit.set_quotient eq2 types.pointed2 .homotopy.smash_adjoint
 
-open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc_index pi group
-     is_trunc function sphere unit sum prod bool
+open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc pi group
+     is_trunc function sphere unit prod bool
 
 namespace eq
 
@@ -93,6 +93,12 @@ namespace eq
   --   (p : f ~ g) (q : a = a') : natural_square p q = square_of_pathover (apd p q) :=
   -- idp
 
+  lemma homotopy_group_isomorphism_of_ptrunc_pequiv {A B : Type*}
+    (n k : ℕ) (H : n+1 ≤[ℕ] k) (f : ptrunc k A ≃* ptrunc k B) : πg[n+1] A ≃g πg[n+1] B :=
+  (ghomotopy_group_ptrunc_of_le H A)⁻¹ᵍ ⬝g
+  homotopy_group_isomorphism_of_pequiv n f ⬝g
+  ghomotopy_group_ptrunc_of_le H B
+
   section hsquare
   variables {A₀₀ A₂₀ A₄₀ A₀₂ A₂₂ A₄₂ A₀₄ A₂₄ A₄₄ : Type}
             {f₁₀ : A₀₀ → A₂₀} {f₃₀ : A₂₀ → A₄₀}
@@ -158,6 +164,13 @@ namespace trunc
 
 end trunc
 
+namespace trunc_index
+  open is_conn nat trunc is_trunc
+  lemma minus_two_add_plus_two (n : ℕ₋₂) : -2+2+n = n :=
+  by induction n with n p; reflexivity; exact ap succ p
+
+end trunc_index
+
 namespace sigma
 
   -- definition sigma_pathover_equiv_of_is_prop {A : Type} {B : A → Type} {C : Πa, B a → Type}
@@ -195,6 +208,9 @@ namespace group
   --   : @is_mul_hom G G' (@ab_group.to_group _ (AbGroup.struct G)) _ φ :=
   -- homomorphism.struct φ
 
+  definition pgroup_of_Group (X : Group) : pgroup X :=
+  pgroup_of_group _ idp
+
   definition isomorphism_ap {A : Type} (F : A → Group) {a b : A} (p : a = b) : F a ≃g F b :=
     isomorphism_of_eq (ap F p)
 
@@ -214,6 +230,17 @@ end group open group
 
 namespace function
   variables {A B : Type} {f f' : A → B}
+  open is_conn sigma.ops
+
+  definition merely_constant {A B : Type} (f : A → B) : Type :=
+  Σb, Πa, merely (f a = b)
+
+  definition merely_constant_pmap {A B : Type*} {f : A →* B} (H : merely_constant f) (a : A) :
+    merely (f a = pt) :=
+  tconcat (tconcat (H.2 a) (tinverse (H.2 pt))) (tr (respect_pt f))
+
+  definition merely_constant_of_is_conn {A B : Type*} (f : A →* B) [is_conn 0 A] : merely_constant f :=
+  ⟨pt, is_conn.elim -1 _ (tr (respect_pt f))⟩
 
   definition homotopy_group_isomorphism_of_is_embedding (n : ℕ) [H : is_succ n] {A B : Type*}
     (f : A →* B) [H2 : is_embedding f] : πg[n] A ≃g πg[n] B :=
@@ -237,21 +264,40 @@ namespace is_conn
 
 end is_conn
 
+namespace is_trunc
+
+open trunc_index is_conn
+
+  definition is_trunc_succ_succ_of_is_trunc_loop (n : ℕ₋₂) (A : Type*) (H : is_trunc (n.+1) (Ω A))
+    (H2 : is_conn 0 A) : is_trunc (n.+2) A :=
+  begin
+    apply is_trunc_succ_of_is_trunc_loop, apply minus_one_le_succ,
+    refine is_conn.elim -1 _ _, exact H
+  end
+  lemma is_trunc_of_is_trunc_loopn (m n : ℕ) (A : Type*) (H : is_trunc n (Ω[m] A))
+    (H2 : is_conn m A) : is_trunc (m +[ℕ] n) A :=
+  begin
+    revert A H H2; induction m with m IH: intro A H H2,
+    { rewrite [nat.zero_add], exact H },
+    rewrite [succ_add],
+    apply is_trunc_succ_succ_of_is_trunc_loop,
+    { apply IH,
+      { apply is_trunc_equiv_closed _ !loopn_succ_in },
+      apply is_conn_loop },
+    exact is_conn_of_le _ (zero_le_of_nat (succ m))
+  end
+
+  lemma is_trunc_of_is_set_loopn (m : ℕ) (A : Type*) (H : is_set (Ω[m] A))
+    (H2 : is_conn m A) : is_trunc m A :=
+  is_trunc_of_is_trunc_loopn m 0 A H H2
+
+end is_trunc
+
 namespace misc
   open is_conn
-  /- move! -/
-  open sigma.ops pointed
-  definition merely_constant {A B : Type} (f : A → B) : Type :=
-  Σb, Πa, merely (f a = b)
 
-  definition merely_constant_pmap {A B : Type*} {f : A →* B} (H : merely_constant f) (a : A) :
-    merely (f a = pt) :=
-  tconcat (tconcat (H.2 a) (tinverse (H.2 pt))) (tr (respect_pt f))
+  open sigma.ops pointed trunc_index
 
-  definition merely_constant_of_is_conn {A B : Type*} (f : A →* B) [is_conn 0 A] : merely_constant f :=
-  ⟨pt, is_conn.elim -1 _ (tr (respect_pt f))⟩
-
-  open sigma
   definition component [constructor] (A : Type*) : Type* :=
   pType.mk (Σ(a : A), merely (pt = a)) ⟨pt, tr idp⟩