From a9fc853985e76fb212da2c085132251a4571c837 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Wed, 23 Nov 2016 23:07:59 -0500
Subject: [PATCH] feat(hott/homotopy/EM): redefine Eilenberg-Maclane spaces and
 prove their uniqueness

---
 hott/homotopy/EM.hlean | 494 +++++++++++++++++++++++++++--------------
 1 file changed, 329 insertions(+), 165 deletions(-)

diff --git a/hott/homotopy/EM.hlean b/hott/homotopy/EM.hlean
index d17c0a906..c3bce08bf 100644
--- a/hott/homotopy/EM.hlean
+++ b/hott/homotopy/EM.hlean
@@ -7,20 +7,20 @@ Authors: Floris van Doorn
 Eilenberg MacLane spaces
 -/
 
-import hit.groupoid_quotient .hopf .freudenthal .homotopy_group
-open algebra pointed nat eq category group algebra is_trunc iso pointed unit trunc equiv is_conn
-     function is_equiv
+import hit.groupoid_quotient homotopy.hopf homotopy.freudenthal homotopy.homotopy_group
+open algebra pointed nat eq category group is_trunc iso unit trunc equiv is_conn function is_equiv
+     trunc_index
 
 namespace EM
   open groupoid_quotient
 
   variables {G : Group}
-  definition EM1 (G : Group) : Type :=
+  definition EM1' (G : Group) : Type :=
   groupoid_quotient (Groupoid_of_Group G)
-  definition pEM1 [constructor] (G : Group) : Type* :=
-  pointed.MK (EM1 G) (elt star)
+  definition EM1 [constructor] (G : Group) : Type* :=
+  pointed.MK (EM1' G) (elt star)
 
-  definition base : EM1 G := elt star
+  definition base : EM1' G := elt star
   definition pth : G → base = base := pth
   definition resp_mul (g h : G) : pth (g * h) = pth g ⬝ pth h := resp_comp h g
   definition resp_one : pth (1 : G) = idp :=
@@ -29,10 +29,11 @@ namespace EM
   definition resp_inv (g : G) : pth (g⁻¹) = (pth g)⁻¹ :=
   resp_inv g
 
-  local attribute pointed.MK pointed.carrier pEM1 EM1 [reducible]
-  protected definition rec {P : EM1 G → Type} [H : Π(x : EM1 G), is_trunc 1 (P x)]
+  local attribute pointed.MK pointed.carrier EM1 EM1' [reducible]
+  protected definition rec {P : EM1' G → Type} [H : Π(x : EM1' G), is_trunc 1 (P x)]
     (Pb : P base) (Pp : Π(g : G), Pb =[pth g] Pb)
-    (Pmul : Π(g h : G), change_path (resp_mul g h) (Pp (g * h)) = Pp g ⬝o Pp h) (x : EM1 G) : P x :=
+    (Pmul : Π(g h : G), change_path (resp_mul g h) (Pp (g * h)) = Pp g ⬝o Pp h) (x : EM1' G) :
+    P x :=
   begin
     induction x,
     { induction g, exact Pb},
@@ -40,27 +41,27 @@ namespace EM
     { induction a, induction b, induction c, exact Pmul f g}
   end
 
-  protected definition rec_on {P : EM1 G → Type} [H : Π(x : EM1 G), is_trunc 1 (P x)]
-    (x : EM1 G) (Pb : P base) (Pp : Π(g : G), Pb =[pth g] Pb)
+  protected definition rec_on {P : EM1' G → Type} [H : Π(x : EM1' G), is_trunc 1 (P x)]
+    (x : EM1' G) (Pb : P base) (Pp : Π(g : G), Pb =[pth g] Pb)
     (Pmul : Π(g h : G), change_path (resp_mul g h) (Pp (g * h)) = Pp g ⬝o Pp h) : P x :=
   EM.rec Pb Pp Pmul x
 
-  protected definition set_rec {P : EM1 G → Type} [H : Π(x : EM1 G), is_set (P x)]
-    (Pb : P base) (Pp : Π(g : G), Pb =[pth g] Pb) (x : EM1 G) : P x :=
+  protected definition set_rec {P : EM1' G → Type} [H : Π(x : EM1' G), is_set (P x)]
+    (Pb : P base) (Pp : Π(g : G), Pb =[pth g] Pb) (x : EM1' G) : P x :=
   EM.rec Pb Pp !center x
 
-  protected definition prop_rec {P : EM1 G → Type} [H : Π(x : EM1 G), is_prop (P x)]
-    (Pb : P base) (x : EM1 G) : P x :=
+  protected definition prop_rec {P : EM1' G → Type} [H : Π(x : EM1' G), is_prop (P x)]
+    (Pb : P base) (x : EM1' G) : P x :=
   EM.rec Pb !center !center x
 
-  definition rec_pth {P : EM1 G → Type} [H : Π(x : EM1 G), is_trunc 1 (P x)]
+  definition rec_pth {P : EM1' G → Type} [H : Π(x : EM1' G), is_trunc 1 (P x)]
     {Pb : P base} {Pp : Π(g : G), Pb =[pth g] Pb}
     (Pmul : Π(g h : G), change_path (resp_mul g h) (Pp (g * h)) = Pp g ⬝o Pp h)
     (g : G) : apd (EM.rec Pb Pp Pmul) (pth g) = Pp g :=
   proof !rec_pth qed
 
   protected definition elim {P : Type} [is_trunc 1 P] (Pb : P) (Pp : Π(g : G), Pb = Pb)
-    (Pmul : Π(g h : G), Pp (g * h) = Pp g ⬝ Pp h) (x : EM1 G) : P :=
+    (Pmul : Π(g h : G), Pp (g * h) = Pp g ⬝ Pp h) (x : EM1' G) : P :=
   begin
     induction x,
     { exact Pb},
@@ -68,15 +69,15 @@ namespace EM
     { exact Pmul f g}
   end
 
-  protected definition elim_on [reducible] {P : Type} [is_trunc 1 P] (x : EM1 G)
+  protected definition elim_on [reducible] {P : Type} [is_trunc 1 P] (x : EM1' G)
     (Pb : P) (Pp : G → Pb = Pb) (Pmul : Π(g h : G), Pp (g * h) = Pp g ⬝ Pp h) : P :=
   EM.elim Pb Pp Pmul x
 
   protected definition set_elim [reducible] {P : Type} [is_set P] (Pb : P) (Pp : G → Pb = Pb)
-    (x : EM1 G) : P :=
+    (x : EM1' G) : P :=
   EM.elim Pb Pp !center x
 
-  protected definition prop_elim [reducible] {P : Type} [is_prop P] (Pb : P) (x : EM1 G) : P :=
+  protected definition prop_elim [reducible] {P : Type} [is_prop P] (Pb : P) (x : EM1' G) : P :=
   EM.elim Pb !center !center x
 
   definition elim_pth {P : Type} [is_trunc 1 P] {Pb : P} {Pp : G → Pb = Pb}
@@ -84,7 +85,7 @@ namespace EM
   proof !elim_pth qed
 
   protected definition elim_set.{u} (Pb : Set.{u}) (Pp : Π(g : G), Pb ≃ Pb)
-    (Pmul : Π(g h : G) (x : Pb), Pp (g * h) x = Pp h (Pp g x)) (x : EM1 G) : Set.{u} :=
+    (Pmul : Π(g h : G) (x : Pb), Pp (g * h) x = Pp h (Pp g x)) (x : EM1' G) : Set.{u} :=
   groupoid_quotient.elim_set (λu, Pb) (λu v, Pp) (λu v w g h, proof Pmul h g qed) x
 
   theorem elim_set_pth {Pb : Set} {Pp : Π(g : G), Pb ≃ Pb}
@@ -104,10 +105,10 @@ namespace EM
   open groupoid_quotient
 
   variables (G : Group)
-  definition base_eq_base_equiv [constructor] : (base = base :> pEM1 G) ≃ G :=
+  definition base_eq_base_equiv : (base = base :> EM1 G) ≃ G :=
   !elt_eq_elt_equiv
 
-  definition fundamental_group_pEM1 : π₁ (pEM1 G) ≃g G :=
+  definition fundamental_group_EM1 : π₁ (EM1 G) ≃g G :=
   begin
     fapply isomorphism_of_equiv,
     { exact trunc_equiv_trunc 0 !base_eq_base_equiv ⬝e trunc_equiv 0 G},
@@ -115,36 +116,85 @@ namespace EM
       exact encode_con p q}
   end
 
-  proposition is_trunc_pEM1 [instance] : is_trunc 1 (pEM1 G) :=
-  !is_trunc_groupoid_quotient
-
   proposition is_trunc_EM1 [instance] : is_trunc 1 (EM1 G) :=
   !is_trunc_groupoid_quotient
 
-  proposition is_conn_EM1 [instance] : is_conn 0 (EM1 G) :=
+  proposition is_trunc_EM1' [instance] : is_trunc 1 (EM1' G) :=
+  !is_trunc_groupoid_quotient
+
+  proposition is_conn_EM1' [instance] : is_conn 0 (EM1' G) :=
   by apply @is_conn_groupoid_quotient; esimp; exact _
 
-  proposition is_conn_pEM1 [instance] : is_conn 0 (pEM1 G) :=
-  is_conn_EM1 G
-  variable {G}
+  proposition is_conn_EM1 [instance] : is_conn 0 (EM1 G) :=
+  is_conn_EM1' G
 
-  definition EM1_map [unfold 7] {X : Type*} (e : Ω X ≃ G)
-    (r : Πp q, e (p ⬝ q) = e p * e q) [is_conn 0 X] [is_trunc 1 X] : EM1 G → X :=
+  variable {G}
+  definition EM1_map [unfold 7] {X : Type*} (e : G → Ω X)
+    (r : Πg h, e (g * h) = e g ⬝ e h) [is_conn 0 X] [is_trunc 1 X] : EM1 G → X :=
   begin
     intro x, induction x using EM.elim,
-    { exact Point X},
-    { exact e⁻¹ᵉ g},
-    { exact inv_preserve_binary e concat mul r g h}
+    { exact Point X },
+    { exact e g },
+    { exact r g h }
   end
 
+  /- Uniqueness of K(G, 1) -/
+
+  definition EM1_pmap [constructor] {X : Type*} (e : G → Ω X)
+    (r : Πg h, e (g * h) = e g ⬝ e h) [is_conn 0 X] [is_trunc 1 X] : EM1 G →* X :=
+  pmap.mk (EM1_map e r) idp
+
+  variable (G)
+  definition loop_EM1 [constructor] : G ≃* Ω (EM1 G) :=
+  (pequiv_of_equiv (base_eq_base_equiv G) idp)⁻¹ᵉ*
+
+  variable {G}
+  definition loop_EM1_pmap {X : Type*} (e : G →* Ω X)
+    (r : Πg h, e (g * h) = e g ⬝ e h) [is_conn 0 X] [is_trunc 1 X] :
+    Ω→(EM1_pmap e r) ∘* loop_EM1 G ~* e :=
+  begin
+    fapply phomotopy.mk,
+    { intro g, refine !idp_con ⬝ elim_pth r g },
+    { apply is_set.elim }
+  end
+
+  definition EM1_pequiv'.{u} {G : Group.{u}} {X : pType.{u}} (e : G ≃* Ω X)
+    (r : Πg h, e (g * h) = e g ⬝ e h) [is_conn 0 X] [is_trunc 1 X] : EM1 G ≃* X :=
+  begin
+    apply pequiv_of_pmap (EM1_pmap e r),
+    apply whitehead_principle_pointed 1,
+    intro k, cases k with k,
+    { apply @is_equiv_of_is_contr,
+      all_goals (esimp; exact _)},
+    { cases k with k,
+      { apply is_equiv_trunc_functor, esimp,
+        apply is_equiv.homotopy_closed, rotate 1,
+        { symmetry, exact phomotopy_pinv_right_of_phomotopy (loop_EM1_pmap _ _) },
+        apply is_equiv_compose e },
+      { apply @is_equiv_of_is_contr,
+        do 2 exact trivial_homotopy_group_of_is_trunc _ (succ_lt_succ !zero_lt_succ)}}
+  end
+
+  definition EM1_pequiv.{u} {G : Group.{u}} {X : pType.{u}} (e : G ≃g π₁ X)
+    [is_conn 0 X] [is_trunc 1 X] : EM1 G ≃* X :=
+  begin
+    apply EM1_pequiv' (pequiv_of_isomorphism e ⬝e* ptrunc_pequiv 0 (Ω X)),
+    refine is_equiv.preserve_binary_of_inv_preserve _ mul concat _,
+    intro p q,
+    exact to_respect_mul e⁻¹ᵍ (tr p) (tr q)
+  end
+
+  definition EM1_pequiv_type (X : Type*) [is_conn 0 X] [is_trunc 1 X] : EM1 (π₁ X) ≃* X :=
+  EM1_pequiv !isomorphism.refl
+
 end EM
 
 open hopf susp
 namespace EM
-  -- The K(G,n+1):
+  /- EM1 G is an h-space if G is an abelian group. This allows us to construct K(G,n) for n ≥ 2 -/
   variables {G : CommGroup} (n : ℕ)
 
-  definition EM1_mul [unfold 2 3] (x x' : EM1 G) : EM1 G :=
+  definition EM1_mul [unfold 2 3] (x x' : EM1' G) : EM1' G :=
   begin
     induction x,
     { exact x'},
@@ -153,18 +203,18 @@ namespace EM
       { exact abstract begin apply loop_pathover, apply square_of_eq,
           refine !resp_mul⁻¹ ⬝ _ ⬝ !resp_mul,
           exact ap pth !mul.comm end end}},
-    { refine EM.prop_rec _ x', apply resp_mul}
+    { refine EM.prop_rec _ x', apply resp_mul }
   end
 
   variable (G)
-  definition EM1_mul_one (x : EM1 G) : EM1_mul x base = x :=
+  definition EM1_mul_one (x : EM1' G) : EM1_mul x base = x :=
   begin
     induction x using EM.set_rec,
     { reflexivity},
     { apply eq_pathover_id_right, apply hdeg_square, refine EM.elim_pth _ g}
   end
 
-  definition h_space_EM1 [constructor] [instance] : h_space (pEM1 G) :=
+  definition h_space_EM1 [constructor] [instance] : h_space (EM1' G) :=
   begin
     fapply h_space.mk,
     { exact EM1_mul},
@@ -174,45 +224,173 @@ namespace EM
   end
 
   /- K(G, n+1) -/
-  definition EMadd1 (n : ℕ) : Type* :=
-  ptrunc (n+1) (iterate_psusp n (pEM1 G))
+  definition EMadd1 : ℕ → Type*
+  | 0 := EM1 G
+  | (n+1) := ptrunc (n+2) (psusp (EMadd1 n))
 
-  definition loop_EM2 : Ω[1] (EMadd1 G 1) ≃* pEM1 G :=
+  definition EMadd1_succ [unfold_full] (n : ℕ) :
+    EMadd1 G (succ n) = ptrunc (n.+2) (psusp (EMadd1 G n)) :=
+  idp
+
+  definition loop_EM2 : Ω[1] (EMadd1 G 1) ≃* EM1 G :=
+  hopf.delooping (EM1' G) idp
+
+  definition is_conn_EMadd1 [instance] (n : ℕ) : is_conn n (EMadd1 G n) :=
   begin
-    apply hopf.delooping, reflexivity
+    induction n with n IH,
+    { apply is_conn_EM1 },
+    { rewrite EMadd1_succ, esimp, exact _ }
   end
 
-  definition homotopy_group_EM2 : πg[1+1] (EMadd1 G 1) ≃g G :=
-  begin
-    refine ghomotopy_group_succ_in _ 0 ⬝g _,
-    refine homotopy_group_isomorphism_of_pequiv 0 (loop_EM2 G) ⬝g _,
-    apply fundamental_group_pEM1
-  end
-
-  definition homotopy_group_EMadd1 (n : ℕ) : πg[n+1] (EMadd1 G n) ≃g G :=
+  definition is_trunc_EMadd1 [instance] (n : ℕ) : is_trunc (n+1) (EMadd1 G n) :=
   begin
     cases n with n,
-    { refine homotopy_group_isomorphism_of_pequiv 0 _ ⬝g fundamental_group_pEM1 G,
-      apply ptrunc_pequiv, apply is_trunc_pEM1},
-    induction n with n IH,
-    { apply homotopy_group_EM2 G},
-    refine _ ⬝g IH,
-    refine !ghomotopy_group_ptrunc ⬝g _ ⬝g !ghomotopy_group_ptrunc⁻¹ᵍ,
-    apply iterate_psusp_stability_isomorphism,
-    rexact add_mul_le_mul_add n 1 1
+    { apply is_trunc_EM1 },
+    { apply is_trunc_trunc }
   end
 
-  section
-    local attribute EMadd1 [reducible]
-    definition is_conn_EMadd1 [instance] (n : ℕ) : is_conn n (EMadd1 G n) := _
-
-    definition is_trunc_EMadd1 [instance] (n : ℕ) : is_trunc (n+1) (EMadd1 G n) :=
-    _
+  /- loops of an EM-space -/
+  definition loop_EMadd1 (n : ℕ) : EMadd1 G n ≃* Ω (EMadd1 G (succ n))  :=
+  begin
+    cases n with n,
+    { exact !loop_EM2⁻¹ᵉ* },
+    { rewrite [EMadd1_succ G (succ n)],
+      refine (ptrunc_pequiv (succ n + 1) _)⁻¹ᵉ*  ⬝e* _ ⬝e* (loop_ptrunc_pequiv _ _)⁻¹ᵉ*,
+      have succ n + 1 ≤ 2 * succ n, from add_mul_le_mul_add n 1 1,
+      refine freudenthal_pequiv _ this }
   end
 
+  definition loopn_EMadd1_pequiv_EM1 (G : CommGroup) (n : ℕ) : EM1 G ≃* Ω[n] (EMadd1 G n) :=
+  begin
+    induction n with n e,
+    { reflexivity },
+    { refine _ ⬝e* !loopn_succ_in⁻¹ᵉ*,
+      refine _ ⬝e* loopn_pequiv_loopn n !loop_EMadd1,
+      exact e }
+  end
+
+  -- use loopn_EMadd1_pequiv_EM1 in this definition?
+  definition loopn_EMadd1 (G : CommGroup) (n : ℕ) : G ≃* Ω[succ n] (EMadd1 G n) :=
+  begin
+    induction n with n e,
+    { apply loop_EM1 },
+    { refine _ ⬝e* !loopn_succ_in⁻¹ᵉ*,
+      refine _ ⬝e* loopn_pequiv_loopn (succ n) !loop_EMadd1,
+      exact e }
+  end
+
+  definition loopn_EMadd1_succ [unfold_full] (G : CommGroup) (n : ℕ) : loopn_EMadd1 G (succ n) ~*
+    !loopn_succ_in⁻¹ᵉ* ∘* apn (succ n) !loop_EMadd1 ∘* loopn_EMadd1 G n :=
+  by reflexivity
+
+  definition EM_up {G : CommGroup} {X : Type*} {n : ℕ} (e : Ω[succ (succ n)] X ≃* G)
+    : Ω[succ n] (Ω X) ≃* G :=
+  !loopn_succ_in⁻¹ᵉ* ⬝e* e
+
+  definition is_homomorphism_EM_up {G : CommGroup} {X : Type*} {n : ℕ}
+    (e : Ω[succ (succ n)] X ≃* G)
+    (r : Π(p q : Ω[succ (succ n)] X), e (p ⬝ q) = e p * e q)
+    (p q : Ω[succ n] (Ω X)) : EM_up e (p ⬝ q) = EM_up e p * EM_up e q :=
+  begin
+    refine _ ⬝ !r, apply ap e, esimp, apply apn_con
+  end
+
+  definition EMadd1_pmap [unfold 8] {G : CommGroup} {X : Type*} (n : ℕ)
+    (e : Ω[succ n] X ≃* G)
+    (r : Πp q, e (p ⬝ q) = e p * e q)
+    [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : EMadd1 G n →* X :=
+  begin
+    revert X e r H1 H2, induction n with n f: intro X e r H1 H2,
+    { exact EM1_pmap e⁻¹ᵉ* (equiv.inv_preserve_binary e concat mul r) },
+    rewrite [EMadd1_succ],
+    exact ptrunc.elim ((succ n).+1)
+            (psusp.elim (f _ (EM_up e) (is_homomorphism_EM_up e r) _ _)),
+  end
+
+  definition EMadd1_pmap_succ {G : CommGroup} {X : Type*} (n : ℕ) (e : Ω[succ (succ n)] X ≃* G)
+    r [H1 : is_conn (succ n) X] [H2 : is_trunc ((succ n).+1) X] : EMadd1_pmap (succ n) e r =
+    ptrunc.elim ((succ n).+1) (psusp.elim (EMadd1_pmap n (EM_up e) (is_homomorphism_EM_up e r))) :=
+  by reflexivity
+
+  definition loop_EMadd1_pmap {G : CommGroup} {X : Type*} {n : ℕ} (e : Ω[succ (succ n)] X ≃* G)
+    (r : Πp q, e (p ⬝ q) = e p * e q)
+    [H1 : is_conn (succ n) X] [H2 : is_trunc ((succ n).+1) X] :
+    Ω→(EMadd1_pmap (succ n) e r) ∘* loop_EMadd1 G n ~*
+    EMadd1_pmap n (EM_up e) (is_homomorphism_EM_up e r) :=
+  begin
+    cases n with n,
+    { apply hopf_delooping_elim },
+    { refine !passoc⁻¹* ⬝* _,
+      rewrite [EMadd1_pmap_succ (succ n)],
+      refine pwhisker_right _ !ap1_ptrunc_elim ⬝* _,
+      refine !passoc⁻¹* ⬝* _,
+      refine pwhisker_right _ (ptrunc_elim_freudenthal_pequiv
+                                (succ n) (succ (succ n)) (add_mul_le_mul_add n 1 1) _) ⬝* _,
+      reflexivity }
+  end
+
+  definition loopn_EMadd1_pmap' {G : CommGroup} {X : Type*} {n : ℕ} (e : Ω[succ n] X ≃* G)
+    (r : Πp q, e (p ⬝ q) = e p * e q)
+    [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] :
+    Ω→[succ n](EMadd1_pmap n e r) ∘* loopn_EMadd1 G n ~* e⁻¹ᵉ* :=
+  begin
+    revert X e r H1 H2, induction n with n IH: intro X e r H1 H2,
+    { apply loop_EM1_pmap },
+    refine pwhisker_left _ !loopn_EMadd1_succ ⬝* _,
+    refine !passoc⁻¹* ⬝* _,
+    refine pwhisker_right _ !loopn_succ_in_inv_natural ⬝* _,
+    refine !passoc ⬝* _,
+    refine pwhisker_left _ (!passoc⁻¹* ⬝*
+             pwhisker_right _ (!apn_pcompose⁻¹* ⬝* apn_phomotopy _ !loop_EMadd1_pmap) ⬝*
+             !IH ⬝* !pinv_trans_pinv_left) ⬝* _,
+    apply pinv_pcompose_cancel_left
+  end
+
+  definition EMadd1_pequiv' {G : CommGroup} {X : Type*} (n : ℕ) (e : Ω[succ n] X ≃* G)
+    (r : Π(p q : Ω[succ n] X), e (p ⬝ q) = e p * e q)
+    [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : EMadd1 G n ≃* X :=
+  begin
+    apply pequiv_of_pmap (EMadd1_pmap n e r),
+    have is_conn 0 (EMadd1 G n), from is_conn_of_le _ (zero_le_of_nat n),
+    have is_trunc (n.+1) (EMadd1 G n), from !is_trunc_EMadd1,
+    refine whitehead_principle_pointed (n.+1) _ _,
+    intro k, apply @nat.lt_by_cases k (succ n): intro H,
+    { apply @is_equiv_of_is_contr,
+      do 2 exact trivial_homotopy_group_of_is_conn _ (le_of_lt_succ H)},
+    { cases H, esimp, apply is_equiv_trunc_functor, esimp,
+      apply is_equiv.homotopy_closed, rotate 1,
+      { symmetry, exact phomotopy_pinv_right_of_phomotopy (loopn_EMadd1_pmap' _ _) },
+      apply is_equiv_compose (e⁻¹ᵉ*)},
+    { apply @is_equiv_of_is_contr,
+      do 2 exact trivial_homotopy_group_of_is_trunc _ H}
+  end
+
+  definition EMadd1_pequiv {G : CommGroup} {X : Type*} (n : ℕ) (e : πg[n+1] X ≃g G)
+    [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : EMadd1 G n ≃* X :=
+  begin
+    have is_set (Ω[succ n] X), from !is_set_loopn,
+    apply EMadd1_pequiv' n ((ptrunc_pequiv _ _)⁻¹ᵉ* ⬝e* pequiv_of_isomorphism e),
+    intro p q, esimp, exact to_respect_mul e (tr p) (tr q)
+  end
+
+  definition EMadd1_pequiv_succ {G : CommGroup} {X : Type*} (n : ℕ) (e : πag[n+2] X ≃g G)
+    [H1 : is_conn (n.+1) X] [H2 : is_trunc (n.+2) X] : EMadd1 G (succ n) ≃* X :=
+  EMadd1_pequiv (succ n) e
+
+  definition ghomotopy_group_EMadd1 (n : ℕ) : πg[n+1] (EMadd1 G n) ≃g G :=
+  begin
+    change π₁ (Ω[n] (EMadd1 G n)) ≃g G,
+    refine homotopy_group_isomorphism_of_pequiv 0 (loopn_EMadd1_pequiv_EM1 G n)⁻¹ᵉ* ⬝g _,
+    apply fundamental_group_EM1,
+  end
+
+  definition EMadd1_pequiv_type (X : Type*) (n : ℕ) [is_conn (n+1) X] [is_trunc (n+1+1) X]
+    : EMadd1 (πag[n+2] X) (succ n) ≃* X :=
+  EMadd1_pequiv_succ n !isomorphism.refl
+
   /- K(G, n) -/
   definition EM (G : CommGroup) : ℕ → Type*
-  | 0     := pType_of_Group G
+  | 0     := G
   | (k+1) := EMadd1 G k
 
   namespace ops
@@ -220,15 +398,15 @@ namespace EM
   end ops
   open ops
 
-  definition homotopy_group_EM (n : ℕ) : π[n] (EM G n) ≃* pType_of_Group G :=
+  definition homotopy_group_EM (n : ℕ) : π[n] (EM G n) ≃* G :=
   begin
     cases n with n,
-    { rexact ptrunc_pequiv 0 (pType_of_Group G) _},
-    { apply pequiv_of_isomorphism (homotopy_group_EMadd1 G n)}
+    { rexact ptrunc_pequiv 0 (G) },
+    { exact pequiv_of_isomorphism (ghomotopy_group_EMadd1 G n)}
   end
 
   definition ghomotopy_group_EM (n : ℕ) : πg[n+1] (EM G (n+1)) ≃g G :=
-  homotopy_group_EMadd1 G n
+  ghomotopy_group_EMadd1 G n
 
   definition is_conn_EM [instance] (n : ℕ) : is_conn (n.-1) (EM G n) :=
   begin
@@ -247,102 +425,88 @@ namespace EM
     { apply is_trunc_EMadd1}
   end
 
-  /- Uniqueness of K(G, 1) -/
-  variable {H : Group}
-  definition pEM1_pmap [constructor] {X : Type*} (e : Ω X ≃ H)
-    (r : Πp q, e (p ⬝ q) = e p * e q) [is_conn 0 X] [is_trunc 1 X] : pEM1 H →* X :=
-  begin
-    apply pmap.mk (EM1_map e r),
-    reflexivity,
-  end
-
-  variable (H)
-  definition loop_pEM1 [constructor] : Ω (pEM1 H) ≃* pType_of_Group H :=
-  pequiv_of_equiv (base_eq_base_equiv H) idp
-
-  variable {H}
-  definition loop_pEM1_pmap {X : Type*} (e : Ω X ≃ H)
-    (r : Πp q, e (p ⬝ q) = e p * e q) [is_conn 0 X] [is_trunc 1 X] :
-    Ω→(pEM1_pmap e r) ~ e⁻¹ᵉ ∘ base_eq_base_equiv H :=
-  begin
-    apply homotopy_of_inv_homotopy_pre (base_eq_base_equiv H),
-    intro g, exact !idp_con ⬝ !elim_pth
-  end
-
-  open trunc_index
-  definition pEM1_pequiv'.{u} {G : Group.{u}} {X : pType.{u}} (e : Ω X ≃ G)
-    (r : Πp q, e (p ⬝ q) = e p * e q) [is_conn 0 X] [is_trunc 1 X] : pEM1 G ≃* X :=
-  begin
-    apply pequiv_of_pmap (pEM1_pmap e r),
-    apply whitehead_principle_pointed 1,
-    intro k, cases k with k,
-    { apply @is_equiv_of_is_contr,
-      all_goals (esimp; exact _)},
-    { cases k with k,
-      { apply is_equiv_trunc_functor, esimp,
-        apply is_equiv.homotopy_closed, rotate 1,
-        { symmetry, exact loop_pEM1_pmap _ _},
-        apply is_equiv_compose, apply to_is_equiv},
-      { apply @is_equiv_of_is_contr,
-        do 2 exact trivial_homotopy_group_of_is_trunc _ (succ_lt_succ !zero_lt_succ)}}
-  end
-
-  definition pEM1_pequiv.{u} {G : Group.{u}} {X : pType.{u}} (e : π₁ X ≃g G)
-    [is_conn 0 X] [is_trunc 1 X] : pEM1 G ≃* X :=
-  begin
-    apply pEM1_pequiv' (!trunc_equiv⁻¹ᵉ ⬝e equiv_of_isomorphism e),
-    intro p q, esimp, exact to_respect_mul e (tr p) (tr q)
-  end
-
-  definition pEM1_pequiv_type {X : Type*} [is_conn 0 X] [is_trunc 1 X] : pEM1 (π₁ X) ≃* X :=
-  pEM1_pequiv !isomorphism.refl
-
-  definition EM_pequiv_1.{u} {G : CommGroup.{u}} {X : pType.{u}} (e : π₁ X ≃g G)
-    [is_conn 0 X] [is_trunc 1 X] : EM G 1 ≃* X :=
-  begin
-    refine _ ⬝e* pEM1_pequiv e,
-    apply ptrunc_pequiv,
-    apply is_trunc_pEM1
-  end
-
-  variable (G)
-  definition EMadd1_pequiv_pEM1 : EMadd1 G 0 ≃* pEM1 G :=
-  begin apply ptrunc_pequiv, apply is_trunc_pEM1 end
-
-  definition EM1add1_pequiv_0.{u} {G : CommGroup.{u}} {X : pType.{u}}
-    (e : π₁ X ≃g G) [is_conn 0 X] [is_trunc 1 X] : EMadd1 G 0 ≃* X :=
-  EMadd1_pequiv_pEM1 G ⬝e* pEM1_pequiv e
-
-  definition KG1_pequiv.{u} {X Y : pType.{u}} (e : π₁ X ≃g π₁ Y)
-    [is_conn 0 X] [is_trunc 1 X] [is_conn 0 Y] [is_trunc 1 Y] : X ≃* Y :=
-  (pEM1_pequiv e)⁻¹ᵉ* ⬝e* pEM1_pequiv !isomorphism.refl
-
-  open circle int
-  definition EM_pequiv_circle : K agℤ 1 ≃* S¹* :=
-  !EMadd1_pequiv_pEM1 ⬝e* pEM1_pequiv fundamental_group_of_circle
-
-  /- loops of EM-spaces -/
-  variable {G}
-  definition loop_EMadd1 (n : ℕ) : Ω (EMadd1 G (succ n)) ≃* EMadd1 G n :=
-  begin
-    cases n with n,
-    { symmetry, apply EM1add1_pequiv_0, rexact homotopy_group_EMadd1 G 1,
-      -- apply is_conn_loop, apply is_conn_EMadd1,
-      apply is_trunc_loop, apply is_trunc_EMadd1},
-    { refine loop_ptrunc_pequiv _ _ ⬝e* _,
-      rewrite [add_one, succ_sub_two],
-      have succ n + 1 ≤ 2 * succ n, from add_mul_le_mul_add n 1 1,
-      symmetry, refine freudenthal_pequiv _ this, }
-  end
-
-  variable (G)
   definition loop_EM (n : ℕ) : Ω (K G (succ n)) ≃* K G n :=
   begin
     cases n with n,
-    { refine _ ⬝e* pequiv_of_isomorphism (fundamental_group_pEM1 G),
-      refine loop_pequiv_loop (EMadd1_pequiv_pEM1 G) ⬝e* _,
-      symmetry, apply ptrunc_pequiv, exact _},
-    { apply loop_EMadd1}
+    { refine _ ⬝e* pequiv_of_isomorphism (fundamental_group_EM1 G),
+      symmetry, apply ptrunc_pequiv },
+    { exact !loop_EMadd1⁻¹ᵉ* }
   end
 
+  open circle int
+  definition EM_pequiv_circle : K agℤ 1 ≃* S¹* :=
+  EM1_pequiv fundamental_group_of_circle⁻¹ᵍ
+
+  /- Functorial action of Eilenberg-Maclane spaces -/
+
+  definition EM1_functor [constructor] {G H : Group} (φ : G →g H) : EM1 G →* EM1 H :=
+  begin
+    fconstructor,
+    { intro g, induction g,
+      { exact base },
+      { exact pth (φ g) },
+      { exact ap pth (to_respect_mul φ g h) ⬝ resp_mul (φ g) (φ h) }},
+    { reflexivity }
+  end
+
+  definition EMadd1_functor [constructor] {G H : CommGroup} (φ : G →g H) (n : ℕ) :
+    EMadd1 G n →* EMadd1 H n :=
+  begin
+    induction n with n ψ,
+    { exact EM1_functor φ },
+    { apply ptrunc_functor, apply psusp_functor, exact ψ }
+  end
+
+  definition EM_functor [unfold 4] {G H : CommGroup} (φ : G →g H) (n : ℕ) :
+    K G n →* K H n :=
+  begin
+    cases n with n,
+    { exact pmap_of_homomorphism φ },
+    { exact EMadd1_functor φ n }
+  end
+
+  -- TODO: (K G n →* K H n) ≃ (G →g H)
+
+  /- Equivalence of Groups and pointed connected 1-truncated types -/
+
+  definition ptruncconntype10_pequiv (X Y : 1-Type*[0]) (e : π₁ X ≃g π₁ Y) : X ≃* Y :=
+  (EM1_pequiv !isomorphism.refl)⁻¹ᵉ* ⬝e* EM1_pequiv e
+
+  definition EM1_pequiv_ptruncconntype10 (X : 1-Type*[0]) : EM1 (π₁ X) ≃* X :=
+  EM1_pequiv_type X
+
+  definition Group_equiv_ptruncconntype10 [constructor] : Group ≃ 1-Type*[0] :=
+  equiv.MK (λG, ptruncconntype.mk (EM1 G) _ pt !is_conn_EM1)
+           (λX, π₁ X)
+           begin intro X, apply ptruncconntype_eq, esimp, exact EM1_pequiv_type X end
+           begin intro G, apply eq_of_isomorphism, apply fundamental_group_EM1 end
+
+  /- Equivalence of CommGroups and pointed n-connected (n+1)-truncated types (n ≥ 1) -/
+
+  open trunc_index
+  definition ptruncconntype_pequiv : Π(n : ℕ) (X Y : (n.+1)-Type*[n])
+    (e : πg[n+1] X ≃g πg[n+1] Y), X ≃* Y
+  | 0 X Y e := ptruncconntype10_pequiv X Y e
+  | (succ n) X Y e :=
+  begin
+    refine (EMadd1_pequiv_succ n _)⁻¹ᵉ* ⬝e* EMadd1_pequiv_succ n !isomorphism.refl,
+    exact e
+  end
+
+  definition EM1_pequiv_ptruncconntype (n : ℕ) (X : (n+1+1)-Type*[n+1]) :
+    EMadd1 (πag[n+2] X) (succ n) ≃* X :=
+  EMadd1_pequiv_type X n
+
+  definition CommGroup_equiv_ptruncconntype' [constructor] (n : ℕ) :
+    CommGroup ≃ (n + 1 + 1)-Type*[n+1] :=
+  equiv.MK
+    (λG, ptruncconntype.mk (EMadd1 G (n+1)) _ pt _)
+    (λX, πag[n+2] X)
+    begin intro X, apply ptruncconntype_eq, apply EMadd1_pequiv_type end
+    begin intro G, apply CommGroup_eq_of_isomorphism, exact ghomotopy_group_EMadd1 G (n+1) end
+
+  definition CommGroup_equiv_ptruncconntype [constructor] (n : ℕ) :
+    CommGroup ≃ (n.+2)-Type*[n.+1] :=
+  CommGroup_equiv_ptruncconntype' n
+
 end EM