diff --git a/algebra/subgroup.hlean b/algebra/subgroup.hlean
index 0f64dbf..33e382d 100644
--- a/algebra/subgroup.hlean
+++ b/algebra/subgroup.hlean
@@ -40,7 +40,7 @@ namespace group
   definition full_subgroup.{u} (G : Group.{u}) : subgroup_rel.{u 0} G :=
   begin
     fapply subgroup_rel.mk,
-    { intro g, fapply trunctype.mk, exact unit, exact _}, -- instead of the unit type, we take g = g, because the unit type is in Type₀ and not in Type.{u}
+    { intro g, fapply trunctype.mk, exact unit, exact _ },
     { esimp, constructor },
     { intros g h p q, esimp, constructor },
     { intros g p, esimp, constructor }
diff --git a/colim.hlean b/colim.hlean
index 0d9cd8f..d55460b 100644
--- a/colim.hlean
+++ b/colim.hlean
@@ -419,7 +419,7 @@ namespace seq_colim
   definition decode [unfold 4] (y : seq_colim g) (c : code y) : ι g x = y :=
   begin
     induction y,
-    { esimp at c, exact sorry},
+    { esimp at c, exact sorry },
     { exact sorry }
   end
 
diff --git a/homotopy/EM.hlean b/homotopy/EM.hlean
new file mode 100644
index 0000000..9c1d300
--- /dev/null
+++ b/homotopy/EM.hlean
@@ -0,0 +1,500 @@
+-- Authors: Floris van Doorn
+
+import homotopy.EM ..move_to_lib algebra.category.functor.equivalence ..pointed_pi
+
+open eq equiv is_equiv algebra group nat pointed EM.ops is_trunc trunc susp function is_conn
+
+namespace EM
+
+  definition EMadd1_functor_succ [unfold_full] {G H : AbGroup} (φ : G →g H) (n : ℕ) :
+    EMadd1_functor φ (succ n) ~* ptrunc_functor (n+2) (psusp_functor (EMadd1_functor φ n)) :=
+  by reflexivity
+
+  definition EM1_functor_gid (G : Group) : EM1_functor (gid G) ~* !pid :=
+  begin
+    fapply phomotopy.mk,
+    { intro x, induction x,
+      { reflexivity },
+      { apply eq_pathover_id_right, apply hdeg_square, apply elim_pth, },
+      { apply @is_prop.elim, apply is_trunc_pathover }},
+    { reflexivity },
+  end
+
+  definition EMadd1_functor_gid (G : AbGroup) (n : ℕ) : EMadd1_functor (gid G) n ~* !pid :=
+  begin
+    induction n with n p,
+    { apply EM1_functor_gid },
+    { refine !EMadd1_functor_succ ⬝* _,
+      refine ptrunc_functor_phomotopy _ (psusp_functor_phomotopy p ⬝* !psusp_functor_pid) ⬝* _,
+      apply ptrunc_functor_pid }
+  end
+
+  definition EM_functor_gid (G : AbGroup) (n : ℕ) : EM_functor (gid G) n ~* !pid :=
+  begin
+    cases n with n,
+    { apply pmap_of_homomorphism_gid },
+    { apply EMadd1_functor_gid }
+  end
+
+  definition EM1_functor_gcompose {G H K : Group} (ψ : H →g K) (φ : G →g H) :
+    EM1_functor (ψ ∘g φ) ~* EM1_functor ψ ∘* EM1_functor φ :=
+  begin
+    fapply phomotopy.mk,
+    { intro x, induction x,
+      { reflexivity },
+      { apply eq_pathover, apply hdeg_square, esimp,
+        refine !elim_pth ⬝ _ ⬝ (ap_compose (EM1_functor ψ) _ _)⁻¹,
+        refine _ ⬝ ap02 _ !elim_pth⁻¹, exact !elim_pth⁻¹ },
+      { apply @is_prop.elim, apply is_trunc_pathover }},
+    { reflexivity },
+  end
+
+  definition EMadd1_functor_gcompose {G H K : AbGroup} (ψ : H →g K) (φ : G →g H) (n : ℕ) :
+    EMadd1_functor (ψ ∘g φ) n ~* EMadd1_functor ψ n ∘* EMadd1_functor φ n :=
+  begin
+    induction n with n p,
+    { apply EM1_functor_gcompose },
+    { refine !EMadd1_functor_succ ⬝* _,
+      refine ptrunc_functor_phomotopy _ (psusp_functor_phomotopy p ⬝* !psusp_functor_pcompose) ⬝* _,
+      apply ptrunc_functor_pcompose }
+  end
+
+  definition EM_functor_gcompose {G H K : AbGroup} (ψ : H →g K) (φ : G →g H) (n : ℕ) :
+    EM_functor (ψ ∘g φ) n ~* EM_functor ψ n ∘* EM_functor φ n :=
+  begin
+    cases n with n,
+    { apply pmap_of_homomorphism_gcompose },
+    { apply EMadd1_functor_gcompose }
+  end
+
+  definition EM1_functor_phomotopy {G H : Group} {φ ψ : G →g H} (p : φ ~ ψ) :
+    EM1_functor φ ~* EM1_functor ψ :=
+  begin
+    fapply phomotopy.mk,
+    { intro x, induction x,
+      { reflexivity },
+      { apply eq_pathover, apply hdeg_square, esimp,
+        refine !elim_pth ⬝ _ ⬝ !elim_pth⁻¹, exact ap pth (p g) },
+      { apply @is_prop.elim, apply is_trunc_pathover }},
+    { reflexivity },
+  end
+
+  definition EMadd1_functor_phomotopy {G H : AbGroup} {φ ψ : G →g H} (p : φ ~ ψ) (n : ℕ) :
+    EMadd1_functor φ n ~* EMadd1_functor ψ n :=
+  begin
+    induction n with n q,
+    { exact EM1_functor_phomotopy p },
+    { exact ptrunc_functor_phomotopy _ (psusp_functor_phomotopy q) }
+  end
+
+  definition EM_functor_phomotopy {G H : AbGroup} {φ ψ : G →g H} (p : φ ~ ψ) (n : ℕ) :
+    EM_functor φ n ~* EM_functor ψ n :=
+  begin
+    cases n with n,
+    { exact pmap_of_homomorphism_phomotopy p },
+    { exact EMadd1_functor_phomotopy p n }
+  end
+
+  definition EM_equiv_EM [constructor] {G H : AbGroup} (φ : G ≃g H) (n : ℕ) : K G n ≃* K H n :=
+  begin
+    fapply pequiv.MK,
+    { exact EM_functor φ n },
+    { exact EM_functor φ⁻¹ᵍ n },
+    { intro x, refine (EM_functor_gcompose φ⁻¹ᵍ φ n)⁻¹* x ⬝ _,
+      refine _ ⬝ EM_functor_gid G n x,
+      refine EM_functor_phomotopy _ n x,
+      rexact left_inv φ },
+    { intro x, refine (EM_functor_gcompose φ φ⁻¹ᵍ n)⁻¹* x ⬝ _,
+      refine _ ⬝ EM_functor_gid H n x,
+      refine EM_functor_phomotopy _ n x,
+      rexact right_inv φ }
+  end
+
+  definition is_equiv_EM_functor [constructor] {G H : AbGroup} (φ : G →g H) [H2 : is_equiv φ]
+    (n : ℕ) : is_equiv (EM_functor φ n) :=
+  to_is_equiv (EM_equiv_EM (isomorphism.mk φ H2) n)
+
+  definition fundamental_group_EM1' (G : Group) : G ≃g π₁ (EM1 G) :=
+  (fundamental_group_EM1 G)⁻¹ᵍ
+
+  definition ghomotopy_group_EMadd1' (G : AbGroup) (n : ℕ) : G ≃g πg[n+1] (EMadd1 G n) :=
+  begin
+    change G ≃g π₁ (Ω[n] (EMadd1 G n)),
+    refine _ ⬝g homotopy_group_isomorphism_of_pequiv 0 (loopn_EMadd1_pequiv_EM1 G n),
+    apply fundamental_group_EM1'
+  end
+
+  definition homotopy_group_functor_EM1_functor {G H : Group} (φ : G →g H) :
+    π→g[1] (EM1_functor φ) ∘ fundamental_group_EM1' G ~ fundamental_group_EM1' H ∘ φ :=
+  begin
+    intro g, apply ap tr, exact !idp_con ⬝ !elim_pth,
+  end
+
+  section
+
+  definition ghomotopy_group_EMadd1'_0 (G : AbGroup) :
+    ghomotopy_group_EMadd1' G 0 ~ fundamental_group_EM1' G :=
+  begin
+    refine _ ⬝hty id_compose _,
+    unfold [ghomotopy_group_EMadd1'],
+    apply hwhisker_right (fundamental_group_EM1' G),
+    refine _ ⬝hty trunc_functor_id _ _,
+    exact trunc_functor_homotopy _ ap1_pid,
+  end
+
+  definition loopn_EMadd1_pequiv_EM1_succ (G : AbGroup) (n : ℕ) :
+    loopn_EMadd1_pequiv_EM1 G (succ n) ~* (loopn_succ_in (EMadd1 G (succ n)) n)⁻¹ᵉ* ∘*
+      Ω→[n] (loop_EMadd1 G n) ∘* loopn_EMadd1_pequiv_EM1 G n :=
+  by reflexivity
+
+  -- definition is_trunc_EMadd1' [instance] (G : AbGroup) (n : ℕ) : is_trunc (succ n) (EMadd1 G n) :=
+  -- is_trunc_EMadd1 G n
+
+  definition loop_EMadd1_succ (G : AbGroup) (n : ℕ) :
+    loop_EMadd1 G (n+1) ~* (loop_ptrunc_pequiv (n+1+1) (psusp (EMadd1 G (n+1))))⁻¹ᵉ* ∘*
+    freudenthal_pequiv (EMadd1 G (n+1)) (add_mul_le_mul_add n 1 1) ∘*
+    (ptrunc_pequiv (n+1+1) (EMadd1 G (n+1)))⁻¹ᵉ* :=
+  by reflexivity
+
+  definition ap1_EMadd1_natural {G H : AbGroup} (φ : G →g H) (n : ℕ) :
+    Ω→ (EMadd1_functor φ (succ n)) ∘* loop_EMadd1 G n ~* loop_EMadd1 H n ∘* EMadd1_functor φ n :=
+  begin
+    refine pwhisker_right _ (ap1_phomotopy !EMadd1_functor_succ) ⬝* _,
+    induction n with n IH,
+    { refine pwhisker_left _ !hopf.to_pmap_delooping_pinv ⬝* _ ⬝*
+             pwhisker_right _ !hopf.to_pmap_delooping_pinv⁻¹*,
+      refine !loop_psusp_unit_natural⁻¹* ⬝h* _,
+      apply ap1_psquare,
+      apply ptr_natural },
+    { refine pwhisker_left _ !loop_EMadd1_succ ⬝* _ ⬝* pwhisker_right _ !loop_EMadd1_succ⁻¹*,
+      refine _ ⬝h* !ap1_ptrunc_functor,
+      refine (@(ptrunc_pequiv_natural (n+1+1) _) _ _)⁻¹ʰ* ⬝h* _,
+      refine pwhisker_left _ !to_pmap_freudenthal_pequiv ⬝* _ ⬝*
+             pwhisker_right _ !to_pmap_freudenthal_pequiv⁻¹*,
+      apply ptrunc_functor_psquare,
+      exact !loop_psusp_unit_natural⁻¹* }
+  end
+
+  definition apn_EMadd1_pequiv_EM1_natural {G H : AbGroup} (φ : G →g H) (n : ℕ) :
+    Ω→[n] (EMadd1_functor φ n) ∘* loopn_EMadd1_pequiv_EM1 G n ~*
+    loopn_EMadd1_pequiv_EM1 H n ∘* EM1_functor φ :=
+  begin
+    induction n with n IH,
+    { reflexivity },
+    { refine pwhisker_left _ !loopn_EMadd1_pequiv_EM1_succ ⬝* _,
+      refine _ ⬝* pwhisker_right _ !loopn_EMadd1_pequiv_EM1_succ⁻¹*,
+      refine _ ⬝h* !loopn_succ_in_inv_natural,
+      exact IH ⬝h* (apn_psquare n !ap1_EMadd1_natural) }
+  end
+
+  definition homotopy_group_functor_EMadd1_functor {G H : AbGroup} (φ : G →g H) (n : ℕ) :
+    π→g[n+1] (EMadd1_functor φ n) ∘ ghomotopy_group_EMadd1' G n ~
+    ghomotopy_group_EMadd1' H n ∘ φ :=
+  begin
+    refine hwhisker_left _ (to_fun_isomorphism_trans _ _) ⬝hty _ ⬝hty
+           hwhisker_right _ (to_fun_isomorphism_trans _ _)⁻¹ʰᵗʸ,
+    refine htyhcompose _ (homotopy_group_homomorphism_psquare 1 (apn_EMadd1_pequiv_EM1_natural φ n)),
+    apply homotopy_group_functor_EM1_functor
+  end
+
+  definition homotopy_group_functor_EMadd1_functor' {G H : AbGroup} (φ : G →g H) (n : ℕ) :
+    φ ∘ (ghomotopy_group_EMadd1' G n)⁻¹ᵍ ~
+      (ghomotopy_group_EMadd1' H n)⁻¹ᵍ ∘ π→g[n+1] (EMadd1_functor φ n) :=
+  htyhinverse (homotopy_group_functor_EMadd1_functor φ n)
+
+  definition EM1_pmap_natural {G H : Group} {X Y : Type*} (f : X →* Y) (eX : G → Ω X)
+    (eY : H → Ω Y) (rX : Πg h, eX (g * h) = eX g ⬝ eX h) (rY : Πg h, eY (g * h) = eY g ⬝ eY h)
+    [H1 : is_conn 0 X] [H2 : is_trunc 1 X] [is_conn 0 Y] [is_trunc 1 Y]
+    (φ : G →g H) (p : Ω→ f ∘ eX ~ eY ∘ φ) :
+    f ∘* EM1_pmap eX rX ~* EM1_pmap eY rY ∘* EM1_functor φ :=
+  begin
+    fapply phomotopy.mk,
+    { intro x, induction x using EM.set_rec,
+      { exact respect_pt f },
+      { apply eq_pathover,
+        refine ap_compose f _ _ ⬝ph _ ⬝hp (ap_compose (EM1_pmap eY rY) _ _)⁻¹,
+        refine ap02 _ !elim_pth ⬝ph _ ⬝hp ap02 _ !elim_pth⁻¹,
+        refine _ ⬝hp !elim_pth⁻¹, apply transpose, exact square_of_eq_bot (p g) }},
+    { exact !idp_con⁻¹ }
+  end
+
+  definition EM1_pequiv'_natural {G H : Group} {X Y : Type*} (f : X →* Y) (eX : G ≃* Ω X)
+    (eY : H ≃* Ω Y) (rX : Πg h, eX (g * h) = eX g ⬝ eX h)  (rY : Πg h, eY (g * h) = eY g ⬝ eY h)
+    [H1 : is_conn 0 X] [H2 : is_trunc 1 X] [is_conn 0 Y] [is_trunc 1 Y]
+    (φ : G →g H) (p : Ω→ f ∘ eX ~ eY ∘ φ) :
+    f ∘* EM1_pequiv' eX rX ~* EM1_pequiv' eY rY ∘* EM1_functor φ :=
+  EM1_pmap_natural f eX eY rX rY φ p
+
+  definition EM1_pequiv_natural {G H : Group} {X Y : Type*} (f : X →* Y) (eX : G ≃g π₁ X)
+    (eY : H ≃g π₁ Y) [H1 : is_conn 0 X] [H2 : is_trunc 1 X] [is_conn 0 Y] [is_trunc 1 Y]
+    (φ : G →g H) (p : π→g[1] f ∘ eX ~ eY ∘ φ) :
+    f ∘* EM1_pequiv eX ~* EM1_pequiv eY ∘* EM1_functor φ :=
+  EM1_pequiv'_natural f _ _ _ _ φ
+    begin
+      assert p' : ptrunc_functor 0 (Ω→ f) ∘* pequiv_of_isomorphism eX ~*
+                  pequiv_of_isomorphism eY ∘* pmap_of_homomorphism φ, exact phomotopy_of_homotopy p,
+      exact phcompose p' (ptrunc_pequiv_natural 0 (Ω→ f)),
+    end
+
+  definition EM1_pequiv_type_natural {X Y : Type*} (f : X →* Y) [H1 : is_conn 0 X] [H2 : is_trunc 1 X]
+    [H3 : is_conn 0 Y] [H4 : is_trunc 1 Y] :
+    f ∘* EM1_pequiv_type X ~* EM1_pequiv_type Y ∘* EM1_functor (π→g[1] f) :=
+  begin refine EM1_pequiv_natural f _ _ _ _, reflexivity end
+
+  definition EM_up_natural {G H : AbGroup} (φ : G →g H) {X Y : Type*} (f : X →* Y) {n : ℕ}
+    (eX : Ω[succ (succ n)] X ≃* G) (eY : Ω[succ (succ n)] Y ≃* H) (p : φ ∘ eX ~ eY ∘ Ω→[succ (succ n)] f)
+    : φ ∘ EM_up eX ~ EM_up eY ∘ Ω→[succ n] (Ω→ f) :=
+  begin
+    refine htyhcompose _ p,
+    exact to_homotopy (phinverse (loopn_succ_in_natural (succ n) f)⁻¹*)
+  end
+
+  definition EMadd1_pmap_natural {G H : AbGroup} {X Y : Type*} (f : X →* Y) (n : ℕ) (eX : Ω[succ n] X ≃* G)
+    (eY : Ω[succ n] Y ≃* H) (rX : Πp q, eX (p ⬝ q) = eX p * eX q) (rY : Πp q, eY (p ⬝ q) = eY p * eY q)
+    [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] [H3 : is_conn n Y] [H4 : is_trunc (n.+1) Y]
+    (φ : G →g H) (p : φ ∘ eX ~ eY ∘ Ω→[succ n] f) :
+    f ∘* EMadd1_pmap n eX rX ~* EMadd1_pmap n eY rY ∘* EMadd1_functor φ n :=
+  begin
+    revert X Y f eX eY rX rY H1 H2 H3 H4 p, induction n with n IH: intros,
+    { apply EM1_pmap_natural, exact @htyhinverse _ _ _ _ eX eY _ _ p },
+    { do 2 rewrite [EMadd1_pmap_succ], refine _ ⬝* pwhisker_left _ !EMadd1_functor_succ⁻¹*,
+      refine (ptrunc_elim_pcompose ((succ n).+1) _ _)⁻¹* ⬝* _ ⬝*
+             (ptrunc_elim_ptrunc_functor ((succ n).+1) _ _)⁻¹*,
+      apply ptrunc_elim_phomotopy,
+      refine _ ⬝* !psusp_elim_psusp_functor⁻¹*,
+      refine _ ⬝* psusp_elim_phomotopy (IH _ _ _ _ _ (is_homomorphism_EM_up eX rX) _ (@is_conn_loop _ _ H1)
+                                           (@is_trunc_loop _ _ H2) _ _ (EM_up_natural φ f eX eY p)),
+      apply psusp_elim_natural }
+  end
+
+  definition EMadd1_pequiv'_natural {G H : AbGroup} {X Y : Type*} (f : X →* Y) (n : ℕ) (eX : Ω[succ n] X ≃* G)
+    (eY : Ω[succ n] Y ≃* H) (rX : Πp q, eX (p ⬝ q) = eX p * eX q) (rY : Πp q, eY (p ⬝ q) = eY p * eY q)
+    [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] [is_conn n Y] [is_trunc (n.+1) Y]
+    (φ : G →g H) (p : φ ∘ eX ~ eY ∘ Ω→[succ n] f) :
+     f ∘* EMadd1_pequiv' n eX rX ~* EMadd1_pequiv' n eY rY ∘* EMadd1_functor φ n :=
+  begin rexact EMadd1_pmap_natural f n eX eY rX rY φ p end
+
+  definition EMadd1_pequiv_natural_local_instance {X : Type*} (n : ℕ) [H : is_trunc (n.+1) X] :
+    is_set (Ω[succ n] X) :=
+  @(is_set_loopn (succ n) X) H
+  local attribute EMadd1_pequiv_natural_local_instance [instance]
+
+  definition EMadd1_pequiv_natural {G H : AbGroup} {X Y : Type*} (f : X →* Y) (n : ℕ) (eX : πg[n+1] X ≃g G)
+    (eY : πg[n+1] Y ≃g H) [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] [H3 : is_conn n Y]
+    [H4 : is_trunc (n.+1) Y] (φ : G →g H) (p : φ ∘ eX ~ eY ∘ π→g[n+1] f) :
+    f ∘* EMadd1_pequiv n eX ~* EMadd1_pequiv n eY ∘* EMadd1_functor φ n :=
+  EMadd1_pequiv'_natural f n
+    ((ptrunc_pequiv 0 (Ω[succ n] X))⁻¹ᵉ* ⬝e* pequiv_of_isomorphism eX)
+    ((ptrunc_pequiv 0 (Ω[succ n] Y))⁻¹ᵉ* ⬝e* pequiv_of_isomorphism eY)
+    _ _ φ (htyhcompose (to_homotopy (phinverse (ptrunc_pequiv_natural 0 (Ω→[succ n] f)))) p)
+
+  definition EMadd1_pequiv_succ_natural {G H : AbGroup} {X Y : Type*} (f : X →* Y) (n : ℕ)
+    (eX : πag[n+2] X ≃g G) (eY : πag[n+2] Y ≃g H) [is_conn (n.+1) X] [is_trunc (n.+2) X]
+    [is_conn (n.+1) Y] [is_trunc (n.+2) Y] (φ : G →g H) (p : φ ∘ eX ~ eY ∘ π→g[n+2] f) :
+    f ∘* EMadd1_pequiv_succ n eX ~* EMadd1_pequiv_succ n eY ∘* EMadd1_functor φ (n+1) :=
+  @(EMadd1_pequiv_natural f (succ n) eX eY) _ _ _ _ φ p
+
+  definition EMadd1_pequiv_type_natural {X Y : Type*} (f : X →* Y) (n : ℕ)
+    [H1 : is_conn (n+1) X] [H2 : is_trunc (n+1+1) X] [H3 : is_conn (n+1) Y] [H4 : is_trunc (n+1+1) Y] :
+    f ∘* EMadd1_pequiv_type X n ~* EMadd1_pequiv_type Y n ∘* EMadd1_functor (π→g[n+2] f) (succ n) :=
+  EMadd1_pequiv_succ_natural f n !isomorphism.refl !isomorphism.refl (π→g[n+2] f)
+    proof λa, idp qed
+
+  -- 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
+  --   fapply equiv.MK,
+  --   { intro f, exact π→g[1] f },
+  --   { intro φ, exact EM1_pequiv_type Y ∘* EM1_functor φ ∘* (EM1_pequiv_type X)⁻¹ᵉ* },
+  --   { intro φ, apply homomorphism_eq,
+  --     refine homotopy_group_homomorphism_pcompose _ _ _ ⬝hty _,
+  --     refine hwhisker_left _ (homotopy_group_homomorphism_pcompose _ _ _) ⬝hty _,
+  --     refine (hassoc _ _ _)⁻¹ʰᵗʸ ⬝hty _, exact sorry },
+  --   { intro f, apply eq_of_phomotopy, refine !passoc⁻¹* ⬝* _, apply pinv_right_phomotopy_of_phomotopy,
+  --     exact sorry }
+  -- end
+
+  -- definition EMadd1_functor_equiv' (n : ℕ) (X Y : Type*) [H1 : is_conn (n+1) X] [H2 : is_trunc (n+1+1) X]
+  --   [H3 : is_conn (n+1) Y] [H4 : is_trunc (n+1+1) Y] : (X →* Y) ≃ (πag[n+2] X →g πag[n+2] Y) :=
+  -- begin
+  --   fapply equiv.MK,
+  --   { intro f, exact π→g[n+2] f },
+  --   { intro φ, exact EMadd1_pequiv_type Y n ∘* EMadd1_functor φ (n+1) ∘* (EMadd1_pequiv_type X n)⁻¹ᵉ* },
+  --   { intro φ, apply homomorphism_eq,
+  --     refine homotopy_group_homomorphism_pcompose _ _ _ ⬝hty _,
+  --     refine hwhisker_left _ (homotopy_group_homomorphism_pcompose _ _ _) ⬝hty _,
+  --     intro g, exact sorry },
+  --   { intro f, apply eq_of_phomotopy, refine !passoc⁻¹* ⬝* _, apply pinv_right_phomotopy_of_phomotopy,
+  --     exact !EMadd1_pequiv_type_natural⁻¹* }
+  -- end
+
+  -- definition EM_functor_equiv (n : ℕ) (G H : AbGroup) : (G →g H) ≃ (EMadd1 G (n+1) →* EMadd1 H (n+1)) :=
+  -- begin
+  --   fapply equiv.MK,
+  --   { intro φ, exact EMadd1_functor φ (n+1) },
+  --   { intro f, exact ghomotopy_group_EMadd1 H (n+1) ∘g π→g[n+2] f ∘g (ghomotopy_group_EMadd1 G (n+1))⁻¹ᵍ },
+  --   { intro f, apply homomorphism_eq, },
+  --   { }
+  -- end
+
+
+  -- definition EMadd1_pmap {G : AbGroup} {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 is_set_pmap_ptruncconntype {n : ℕ₋₂} (X Y : (n.+1)-Type*[n]) : is_set (X →* Y) :=
+  -- begin
+  --   apply is_trunc_succ_intro,
+  --   intro f g,
+  --   apply @(is_trunc_equiv_closed_rev -1 (pmap_eq_equiv f g)),
+  --   apply is_prop.mk,
+  --   exact sorry
+  -- end
+
+
+  end
+
+  /- category -/
+  structure ptruncconntype' (n : ℕ₋₂) : Type :=
+   (A : Type*)
+   (H1 : is_conn n A)
+   (H2 : is_trunc (n+1) A)
+
+  attribute ptruncconntype'.A [coercion]
+  attribute ptruncconntype'.H1 ptruncconntype'.H2 [instance]
+
+  definition EM1_pequiv_ptruncconntype' (X : ptruncconntype' 0) : EM1 (πg[1] X) ≃* X :=
+  @(EM1_pequiv_type X) _ (ptruncconntype'.H2 X)
+
+  definition EMadd1_pequiv_ptruncconntype' {n : ℕ} (X : ptruncconntype' (n+1)) :
+    EMadd1 (πag[n+2] X) (succ n) ≃* X :=
+  @(EMadd1_pequiv_type X n) _ (ptruncconntype'.H2 X)
+
+  open trunc_index
+  definition is_set_pmap_ptruncconntype {n : ℕ₋₂} (X Y : ptruncconntype' n) : is_set (X →* Y) :=
+  begin
+    cases n with n, { exact _ },
+    cases Y with Y H1 H2, cases Y with Y y₀,
+    exact is_trunc_pmap X n -1 (ptrunctype.mk Y _ y₀),
+  end
+
+  open category
+  definition precategory_ptruncconntype'.{u} [constructor] (n : ℕ₋₂) :
+    precategory.{u+1 u} (ptruncconntype' n) :=
+  begin
+    fapply precategory.mk,
+    { exact λX Y, X →* Y },
+    { exact is_set_pmap_ptruncconntype },
+    { exact λX Y Z g f, g ∘* f },
+    { exact λX, pid X },
+    { intros, apply eq_of_phomotopy, exact !passoc⁻¹* },
+    { intros, apply eq_of_phomotopy, apply pid_pcompose },
+    { intros, apply eq_of_phomotopy, apply pcompose_pid }
+  end
+
+  definition cptruncconntype' [constructor] (n : ℕ₋₂) : Precategory :=
+  precategory.Mk (precategory_ptruncconntype' n)
+
+  notation `cType*[`:95 n `]`:0 := cptruncconntype' n
+
+  definition tEM1 [constructor] (G : Group) : ptruncconntype' 0 :=
+  ptruncconntype'.mk (EM1 G) _ !is_trunc_EM1
+
+  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)
+    (λG H φ, EM1_functor φ)
+    begin intro, fapply eq_of_phomotopy, apply EM1_functor_gid end
+    begin intros, fapply eq_of_phomotopy, apply EM1_functor_gcompose end
+
+  definition EM_cfunctor (n : ℕ) : AbGrp ⇒ cType*[n.-1] :=
+  functor.mk
+    (λG, tEM G n)
+    (λG H φ, EM_functor φ n)
+    begin intro, fapply eq_of_phomotopy, apply EM_functor_gid end
+    begin intros, fapply eq_of_phomotopy, apply EM_functor_gcompose end
+
+  definition homotopy_group_cfunctor : cType*[0] ⇒ Grp :=
+  functor.mk
+    (λX, πg[1] X)
+    (λX Y f, π→g[1] f)
+    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
+
+  definition ab_homotopy_group_cfunctor (n : ℕ) : cType*[n+2.-1] ⇒ AbGrp :=
+  functor.mk
+    (λX, πag[n+2] X)
+    (λX Y f, π→g[n+2] f)
+    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
+    fapply is_equivalence.mk,
+    { exact homotopy_group_cfunctor.{u} },
+    { fapply natural_iso.mk,
+      { fapply nat_trans.mk,
+        { intro G, exact (fundamental_group_EM1' G)⁻¹ᵍ },
+        { intro G H φ, apply homomorphism_eq, exact htyhinverse (homotopy_group_functor_EM1_functor φ) }},
+      { intro G, fapply iso.is_iso.mk,
+        { exact fundamental_group_EM1' G },
+        { apply homomorphism_eq,
+          exact to_right_inv (equiv_of_isomorphism (fundamental_group_EM1' G)), },
+        { apply homomorphism_eq,
+          exact to_left_inv (equiv_of_isomorphism (fundamental_group_EM1' G)), }}},
+    { fapply natural_iso.mk,
+      { fapply nat_trans.mk,
+        { intro X, exact EM1_pequiv_ptruncconntype' X },
+        { intro X Y f, apply eq_of_phomotopy, apply EM1_pequiv_type_natural }},
+      { intro X, fapply iso.is_iso.mk,
+        { exact (EM1_pequiv_ptruncconntype' X)⁻¹ᵉ* },
+        { apply eq_of_phomotopy, apply pleft_inv },
+        { apply eq_of_phomotopy, apply pright_inv }}}
+  end
+
+  definition is_equivalence_EM_cfunctor (n : ℕ) : is_equivalence (EM_cfunctor (n+2)) :=
+  begin
+    fapply is_equivalence.mk,
+    { exact ab_homotopy_group_cfunctor n },
+    { fapply natural_iso.mk,
+      { fapply nat_trans.mk,
+        { intro G, exact (ghomotopy_group_EMadd1' G (n+1))⁻¹ᵍ },
+        { intro G H φ, apply homomorphism_eq, exact homotopy_group_functor_EMadd1_functor' φ (n+1) }},
+      { intro G, fapply iso.is_iso.mk,
+        { exact ghomotopy_group_EMadd1' G (n+1) },
+        { apply homomorphism_eq,
+          exact to_right_inv (equiv_of_isomorphism (ghomotopy_group_EMadd1' G (n+1))), },
+        { apply homomorphism_eq,
+          exact to_left_inv (equiv_of_isomorphism (ghomotopy_group_EMadd1' G (n+1))), }}},
+    { fapply natural_iso.mk,
+      { fapply nat_trans.mk,
+        { intro X, exact EMadd1_pequiv_ptruncconntype' X },
+        { intro X Y f, apply eq_of_phomotopy, apply EMadd1_pequiv_type_natural }},
+      { intro X, fapply iso.is_iso.mk,
+        { exact (EMadd1_pequiv_ptruncconntype' X)⁻¹ᵉ* },
+        { apply eq_of_phomotopy, apply pleft_inv },
+        { apply eq_of_phomotopy, apply pright_inv }}}
+  end
+
+  definition Grp_equivalence_cptruncconntype'.{u} [constructor] : Grp.{u} ≃c cType*[0] :=
+  equivalence.mk EM1_cfunctor.{u} is_equivalence_EM1_cfunctor.{u}
+
+  definition AbGrp_equivalence_cptruncconntype' [constructor] (n : ℕ) : AbGrp ≃c cType*[n+2.-1] :=
+  equivalence.mk (EM_cfunctor (n+2)) (is_equivalence_EM_cfunctor n)
+
+end EM
diff --git a/homotopy/smash.hlean b/homotopy/smash.hlean
index a8a26eb..bb79785 100644
--- a/homotopy/smash.hlean
+++ b/homotopy/smash.hlean
@@ -1,15 +1,15 @@
 -- Authors: Floris van Doorn
 
-import homotopy.smash
+import homotopy.smash ..move_to_lib
 
 open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber prod.ops wedge
 
-  /- smash A (susp B) = susp (smash A B) <- this follows from associativity and smash with S¹-/
+  /- smash A (susp B) = susp (smash A B) <- this follows from associativity and smash with S¹ -/
 
   /- To prove: Σ(X × Y) ≃ ΣX ∨ ΣY ∨ Σ(X ∧ Y) (notation means suspension, wedge, smash),
      and both are equivalent to the reduced join -/
 
-  /- To prove: commutative, associative -/
+  /- To prove: associative -/
 
   /- smash A B ≃ pcofiber (pprod_of_pwedge A B) -/
 
@@ -71,13 +71,41 @@ namespace smash
     { exact smash_of_pcofiber_glue x }
   end
 
+  set_option pp.binder_types true
+  -- maybe useful lemma:
+  open function pushout
+  definition pushout_glue_natural {A B C D E : Type} {f : A → B} {g : A → C} (a : A)
+    {h₁ : B → D} {k₁ : C → D} (p₁ : h₁ ∘ f ~ k₁ ∘ g)
+    {h₂ : B → E} {k₂ : C → E} (p₂ : h₂ ∘ f ~ k₂ ∘ g) :
+    @square (pushout (pushout.elim h₁ k₁ p₁) (pushout.elim h₂ k₂ p₂)) _ _ _ _
+      (pushout.glue (inl (f a))) (pushout.glue (inr (g a)))
+      (ap pushout.inl (p₁ a)) (ap pushout.inr (p₂ a)) :=
+  begin
+    apply square_of_eq, symmetry,
+    refine _ ⬝ (ap_con_eq_con_ap (pushout.glue) (pushout.glue a)) ⬝ _,
+    apply whisker_right, exact sorry,
+    apply whisker_left, exact sorry
+  end
+
   definition pcofiber_of_smash_of_pcofiber (x : pcofiber (pprod_of_pwedge A B)) :
     pcofiber_of_smash (smash_of_pcofiber x) = x :=
   begin
     induction x with x x,
     { refine (pushout.glue pt)⁻¹ },
-    { exact sorry },
-    { exact sorry }
+    { induction x with a b, reflexivity },
+    { apply eq_pathover_id_right, esimp,
+      refine ap_compose' pcofiber_of_smash smash_of_pcofiber (cofiber.glue x) ⬝ph _,
+      refine ap02 _ !cofiber.elim_glue' ⬝ph _,
+      induction x,
+      { refine (!ap_con ⬝ !elim_gluel ◾ (!ap_inv ⬝ !elim_gluel⁻² ⬝ !inv_inv)) ⬝ph _,
+        apply whisker_tl, apply hrfl },
+      { esimp, refine (!ap_con ⬝ !elim_gluer ◾ (!ap_inv ⬝ !elim_gluer⁻² ⬝ !inv_inv)) ⬝ph _,
+        apply square_of_eq, esimp, apply whisker_right, apply inverse2,
+        refine _ ⬝ (ap_con_eq_con_ap (pushout.glue) (wedge.glue A B))⁻¹ ⬝ _,
+        { apply whisker_left, refine _ ⬝ (ap_compose' pushout.inr _ _)⁻¹,
+          exact ap02 _ !pushout.elim_glue⁻¹ },
+        { refine whisker_right _ _ ⬝ !idp_con, apply ap_constant }},
+      { exact sorry }}
   end
 
   definition smash_of_pcofiber_of_smash (x : smash A B) :
@@ -98,7 +126,7 @@ namespace smash
   end
 
   variables (A B)
-  definition smash_pequiv_pcofiber : smash A B ≃* pcofiber (pprod_of_pwedge A B) :=
+  definition smash_pequiv_pcofiber [constructor] : smash A B ≃* pcofiber (pprod_of_pwedge A B) :=
   begin
     fapply pequiv_of_equiv,
     { fapply equiv.MK,
@@ -106,17 +134,50 @@ namespace smash
       { apply smash_of_pcofiber },
       { exact pcofiber_of_smash_of_pcofiber },
       { exact smash_of_pcofiber_of_smash }},
-    { esimp, symmetry, apply pushout.glue pt }
+    { symmetry, exact pushout.glue (Point (pwedge A B)) }
   end
 
   variables {A B}
 
+  /- commutativity -/
+
+  definition smash_flip (x : smash A B) : smash B A :=
+  begin
+    induction x,
+    { exact smash.mk b a },
+    { exact auxr },
+    { exact auxl },
+    { exact gluer a },
+    { exact gluel b }
+  end
+
+  definition smash_flip_smash_flip (x : smash A B) : smash_flip (smash_flip x) = x :=
+  begin
+    induction x,
+    { reflexivity },
+    { reflexivity },
+    { reflexivity },
+    { apply eq_pathover_id_right,
+      refine ap_compose' smash_flip _ _ ⬝ ap02 _ !elim_gluel ⬝ !elim_gluer ⬝ph _,
+      apply hrfl },
+    { apply eq_pathover_id_right,
+      refine ap_compose' smash_flip _ _ ⬝ ap02 _ !elim_gluer ⬝ !elim_gluel ⬝ph _,
+      apply hrfl }
+  end
+
+  definition smash_comm : smash A B ≃* smash B A :=
+  begin
+    fapply pequiv_of_equiv,
+    { apply equiv.MK, do 2 exact smash_flip_smash_flip },
+    { reflexivity }
+  end
+
   /- smash A S¹ = susp A -/
   open susp
 
   definition psusp_of_smash_pcircle [unfold 2] (x : smash A S¹*) : psusp A :=
   begin
-    induction x,
+    induction x using smash.elim,
     { induction b, exact pt, exact merid a ⬝ (merid pt)⁻¹ },
     { exact pt },
     { exact pt },
@@ -133,7 +194,7 @@ namespace smash
     { exact gluel' pt a ⬝ ap (smash.mk a) loop ⬝ gluel' a pt },
   end
 
-exit -- the definitions below compile, but take a long time to do so and have sorry's in them
+ -- the definitions below compile, but take a long time to do so and have sorry's in them
   definition smash_pcircle_of_psusp_of_smash_pcircle_pt [unfold 3] (a : A) (x : S¹*) :
     smash_pcircle_of_psusp (psusp_of_smash_pcircle (smash.mk a x)) = smash.mk a x :=
   begin
@@ -152,18 +213,19 @@ exit -- the definitions below compile, but take a long time to do so and have so
       refine !ap_mk_right ⬝ !con.right_inv end end }
   end
 
-  definition smash_pcircle_of_psusp_of_smash_pcircle_gluer_base (b : S¹*)
-    : square (smash_pcircle_of_psusp_of_smash_pcircle_pt (Point A) b)
-             (gluer pt)
-             (ap smash_pcircle_of_psusp (ap (λ a, psusp_of_smash_pcircle a) (gluer b)))
-             (gluer b) :=
-  begin
-    refine ap02 _ !elim_gluer ⬝ph _,
-    induction b,
-    { apply square_of_eq, exact whisker_right _ !con.right_inv },
-    { apply square_pathover', exact sorry }
-  end
+  -- definition smash_pcircle_of_psusp_of_smash_pcircle_gluer_base (b : S¹*)
+  --   : square (smash_pcircle_of_psusp_of_smash_pcircle_pt (Point A) b)
+  --            (gluer pt)
+  --            (ap smash_pcircle_of_psusp (ap (λ a, psusp_of_smash_pcircle a) (gluer b)))
+  --            (gluer b) :=
+  -- begin
+  --   refine ap02 _ !elim_gluer ⬝ph _,
+  --   induction b,
+  --   { apply square_of_eq, exact whisker_right _ !con.right_inv },
+  --   { apply square_pathover', exact sorry }
+  -- end
 
+exit
   definition smash_pcircle_pequiv [constructor] (A : Type*) : smash A S¹* ≃* psusp A :=
   begin
     fapply pequiv_of_equiv,
@@ -178,7 +240,8 @@ exit -- the definitions below compile, but take a long time to do so and have so
           refine ap02 _ !elim_merid ⬝ph _,
           rewrite [↑gluel', +ap_con, +ap_inv, -ap_compose'],
           refine (_ ◾ _⁻² ◾ _ ◾ (_ ◾ _⁻²)) ⬝ph _,
-          rotate 5, do 2 apply elim_gluel, esimp, apply elim_loop, do 2 apply elim_gluel,
+          rotate 5, do 2 (unfold [psusp_of_smash_pcircle]; apply elim_gluel),
+          esimp, apply elim_loop, do 2 (unfold [psusp_of_smash_pcircle]; apply elim_gluel),
           refine idp_con (merid a ⬝ (merid (Point A))⁻¹) ⬝ph _,
           apply square_of_eq, refine !idp_con ⬝ _⁻¹, apply inv_con_cancel_right } end end },
       { intro x, induction x using smash.rec,
@@ -187,10 +250,12 @@ exit -- the definitions below compile, but take a long time to do so and have so
         { exact gluer pt },
         { apply eq_pathover_id_right,
           refine ap_compose smash_pcircle_of_psusp _ _ ⬝ph _,
+          unfold [psusp_of_smash_pcircle],
           refine ap02 _ !elim_gluel ⬝ph _,
           esimp, apply whisker_rt, exact vrfl },
         { apply eq_pathover_id_right,
           refine ap_compose smash_pcircle_of_psusp _ _ ⬝ph _,
+          unfold [psusp_of_smash_pcircle],
           refine ap02 _ !elim_gluer ⬝ph _,
           induction b,
           { apply square_of_eq, exact whisker_right _ !con.right_inv },
diff --git a/homotopy/spectrum.hlean b/homotopy/spectrum.hlean
index 63dc0db..bf041d3 100644
--- a/homotopy/spectrum.hlean
+++ b/homotopy/spectrum.hlean
@@ -152,7 +152,7 @@ namespace spectrum
              ~* (glue Z n ∘* to_fun g n) ∘* to_fun f n                 : passoc
          ... ~* (Ω→(to_fun g (S n)) ∘* glue Y n) ∘* to_fun f n      : pwhisker_right (to_fun f n) (glue_square g n)
          ... ~* Ω→(to_fun g (S n)) ∘* (glue Y n ∘* to_fun f n)      : passoc
-         ... ~* Ω→(to_fun g (S n)) ∘* (Ω→ (f (S n)) ∘* glue X n) : pwhisker_left Ω→(to_fun g (S n)) (glue_square f n)
+         ... ~* Ω→(to_fun g (S n)) ∘* (Ω→ (f (S n)) ∘* glue X n) : pwhisker_left (Ω→(to_fun g (S n))) (glue_square f n)
          ... ~* (Ω→(to_fun g (S n)) ∘* Ω→(f (S n))) ∘* glue X n  : passoc
          ... ~* Ω→(to_fun g (S n) ∘* to_fun f (S n)) ∘* glue X n : pwhisker_right (glue X n) (ap1_pcompose _ _))
 
diff --git a/move_to_lib.hlean b/move_to_lib.hlean
index 36e3e87..0ac84bb 100644
--- a/move_to_lib.hlean
+++ b/move_to_lib.hlean
@@ -5,9 +5,301 @@ import homotopy.sphere2 homotopy.cofiber homotopy.wedge
 open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc_index pi group
      is_trunc function sphere
 
+attribute pwedge [constructor]
+attribute is_succ_add_right is_succ_add_left is_succ_bit0 [constructor]
+
+namespace eq
+
+  definition compose_id {A B : Type} (f : A → B) : f ∘ id ~ f :=
+  by reflexivity
+
+  definition id_compose {A B : Type} (f : A → B) : id ∘ f ~ f :=
+  by reflexivity
+
+end eq
+
+namespace cofiber
+
+  -- replace the one in homotopy.cofiber, which has an superfluous argument
+  protected theorem elim_glue' {A B : Type} {f : A → B} {P : Type} (Pbase : P) (Pcod : B → P)
+    (Pglue : Π (x : A), Pbase = Pcod (f x)) (a : A)
+    : ap (cofiber.elim Pbase Pcod Pglue) (cofiber.glue a) = Pglue a :=
+  !pushout.elim_glue
+
+end cofiber
+
+namespace wedge
+  open pushout unit
+  protected definition glue (A B : Type*) : inl pt = inr pt :> wedge A B :=
+  pushout.glue ⋆
+
+end wedge
+
+namespace pointed
+
+  definition to_fun_pequiv_trans {X Y Z : Type*} (f : X ≃* Y) (g :Y ≃* Z) : f ⬝e* g ~ g ∘ f :=
+  λx, idp
+
+  definition pcompose2' {A B C : Type*} {g g' : B →* C} {f f' : A →* B} (q : g ~* g') (p : f ~* f') :
+    g ∘* f ~* g' ∘* f' :=
+  pwhisker_right f q ⬝* pwhisker_left g' p
+
+  infixr ` ◾*' `:80 := pcompose2'
+
+  definition phomotopy_of_homotopy {X Y : Type*} {f g : X →* Y} (h : f ~ g) [is_set Y] : f ~* g :=
+  begin
+    fapply phomotopy.mk,
+    { exact h },
+    { apply is_set.elim }
+  end
+
+  -- /- the pointed type of (unpointed) dependent maps -/
+  -- definition pupi [constructor] {A : Type} (P : A → Type*) : Type* :=
+  -- pointed.mk' (Πa, P a)
+
+  -- definition loop_pupi_commute {A : Type} (B : A → Type*) : Ω(pupi B) ≃* pupi (λa, Ω (B a)) :=
+  -- pequiv_of_equiv eq_equiv_homotopy rfl
+
+  -- definition equiv_pupi_right {A : Type} {P Q : A → Type*} (g : Πa, P a ≃* Q a)
+  --   : pupi P ≃* pupi Q :=
+  -- pequiv_of_equiv (pi_equiv_pi_right g)
+  --   begin esimp, apply eq_of_homotopy, intros a, esimp, exact (respect_pt (g a)) end
+
+  /-
+    Squares of pointed homotopies
+
+    We treat expressions of the form
+      k ∘* f ~* g ∘* h
+    as squares, where f is the top, g is the bottom, h is the left face and k is the right face.
+    Then the following are operations on squares
+  -/
+
+  definition psquare {A B C D : Type*} (f : A →* B) (g : C →* D) (h : A ≃* C) (k : B ≃* D) : Type :=
+  k ∘* f ~* g ∘* h
+
+  definition phcompose {A B C D B' D' : Type*} {f : A →* B} {g : C →* D} {h : A →* C} {k : B →* D}
+    {f' : B →* B'} {g' : D →* D'} {k' : B' →* D'} (p : k ∘* f ~* g ∘* h)
+    (q : k' ∘* f' ~* g' ∘* k) : k' ∘* (f' ∘* f) ~* (g' ∘* g) ∘* h :=
+  !passoc⁻¹* ⬝* pwhisker_right f q ⬝* !passoc ⬝* pwhisker_left g' p ⬝* !passoc⁻¹*
+
+  definition pvcompose {A B C D C' D' : Type*} {f : A →* B} {g : C →* D} {h : A →* C} {k : B →* D}
+    {g' : C' →* D'} {h' : C →* C'} {k' : D →* D'} (p : k ∘* f ~* g ∘* h)
+    (q : k' ∘* g ~* g' ∘* h') : (k' ∘* k) ∘* f ~* g' ∘* (h' ∘* h) :=
+  (phcompose p⁻¹* q⁻¹*)⁻¹*
+
+  definition phinverse {A B C D : Type*} {f : A ≃* B} {g : C ≃* D} {h : A →* C} {k : B →* D}
+    (p : k ∘* f ~* g ∘* h) : h ∘* f⁻¹ᵉ* ~* g⁻¹ᵉ* ∘* k :=
+  !pid_pcompose⁻¹* ⬝* pwhisker_right _ (pleft_inv g)⁻¹* ⬝* !passoc ⬝*
+  pwhisker_left _
+    (!passoc⁻¹* ⬝* pwhisker_right _ p⁻¹* ⬝* !passoc ⬝* pwhisker_left _ !pright_inv ⬝* !pcompose_pid)
+
+  definition pvinverse {A B C D : Type*} {f : A →* B} {g : C →* D} {h : A ≃* C} {k : B ≃* D}
+    (p : k ∘* f ~* g ∘* h) : k⁻¹ᵉ* ∘* g ~* f ∘* h⁻¹ᵉ* :=
+  (phinverse p⁻¹*)⁻¹*
+
+  infix ` ⬝h* `:73 := phcompose
+  infix ` ⬝v* `:73 := pvcompose
+  postfix `⁻¹ʰ*`:(max+1) := phinverse
+  postfix `⁻¹ᵛ*`:(max+1) := pvinverse
+
+  definition ap1_psquare {A B C D : Type*} {f : A →* B} {g : C →* D} {h : A →* C} {k : B →* D}
+    (p : k ∘* f ~* g ∘* h) : Ω→ k ∘* Ω→ f ~* Ω→ g ∘* Ω→ h :=
+  !ap1_pcompose⁻¹* ⬝* ap1_phomotopy p ⬝* !ap1_pcompose
+
+  definition apn_psquare (n : ℕ) {A B C D : Type*} {f : A →* B} {g : C →* D} {h : A →* C} {k : B →* D}
+    (p : k ∘* f ~* g ∘* h) : Ω→[n] k ∘* Ω→[n] f ~* Ω→[n] g ∘* Ω→[n] h :=
+  !apn_pcompose⁻¹* ⬝* apn_phomotopy n p ⬝* !apn_pcompose
+
+  definition ptrunc_functor_psquare (n : ℕ₋₂) {A B C D : Type*} {f : A →* B} {g : C →* D} {h : A →* C}
+    {k : B →* D} (p : k ∘* f ~* g ∘* h) :
+    ptrunc_functor n k ∘* ptrunc_functor n f ~* ptrunc_functor n g ∘* ptrunc_functor n h :=
+  !ptrunc_functor_pcompose⁻¹* ⬝* ptrunc_functor_phomotopy n p ⬝* !ptrunc_functor_pcompose
+
+  definition homotopy_group_homomorphism_psquare (n : ℕ) [H : is_succ n] {A B C D : Type*}
+    {f : A →* B} {g : C →* D} {h : A →* C} {k : B →* D} (p : k ∘* f ~* g ∘* h) :
+    π→g[n] k ∘ π→g[n] f ~ π→g[n] g ∘ π→g[n] h :=
+  begin
+    induction H with n, exact to_homotopy (ptrunc_functor_psquare 0 (apn_psquare (succ n) p))
+  end
+
+  definition htyhcompose {A B C D B' D' : Type} {f : A → B} {g : C → D} {h : A → C} {k : B → D}
+    {f' : B → B'} {g' : D → D'} {k' : B' → D'} (p : k ∘ f ~ g ∘ h)
+    (q : k' ∘ f' ~ g' ∘ k) : k' ∘ (f' ∘ f) ~ (g' ∘ g) ∘ h :=
+  λa, q (f a) ⬝ ap g' (p a)
+
+  definition htyhinverse {A B C D : Type} {f : A ≃ B} {g : C ≃ D} {h : A → C} {k : B → D}
+    (p : k ∘ f ~ g ∘ h) : h ∘ f⁻¹ᵉ ~ g⁻¹ᵉ ∘ k :=
+  λb, eq_inv_of_eq ((p (f⁻¹ᵉ b))⁻¹ ⬝ ap k (to_right_inv f b))
+
+end pointed open pointed
+
+namespace trunc
+
+  -- TODO: redefine loopn_ptrunc_pequiv
+  definition apn_ptrunc_functor (n : ℕ₋₂) (k : ℕ) {A B : Type*} (f : A →* B) :
+    Ω→[k] (ptrunc_functor (n+k) f) ∘* (loopn_ptrunc_pequiv n k A)⁻¹ᵉ* ~*
+    (loopn_ptrunc_pequiv n k B)⁻¹ᵉ* ∘* ptrunc_functor n (Ω→[k] f) :=
+  begin
+    revert n, induction k with k IH: intro n,
+    { reflexivity },
+    { exact sorry }
+  end
+
+  definition ptrunc_pequiv_natural [constructor] (n : ℕ₋₂) {A B : Type*} (f : A →* B) [is_trunc n A]
+    [is_trunc n B] : f ∘* ptrunc_pequiv n A ~* ptrunc_pequiv n B ∘* ptrunc_functor n f :=
+  begin
+    fapply phomotopy.mk,
+    { intro a, induction a with a, reflexivity },
+    { refine !idp_con ⬝ _ ⬝ !idp_con⁻¹, refine !ap_compose'⁻¹ ⬝ _, apply ap_id }
+  end
+
+  definition ptr_natural [constructor] (n : ℕ₋₂) {A B : Type*} (f : A →* B) :
+    ptrunc_functor n f ∘* ptr n A ~* ptr n B ∘* f :=
+  begin
+    fapply phomotopy.mk,
+    { intro a, reflexivity },
+    { reflexivity }
+  end
+
+  definition ptrunc_elim_pcompose (n : ℕ₋₂) {A B C : Type*} (g : B →* C) (f : A →* B) [is_trunc n B]
+    [is_trunc n C] : ptrunc.elim n (g ∘* f) ~* g ∘* ptrunc.elim n f :=
+  begin
+    fapply phomotopy.mk,
+    { intro a, induction a with a, reflexivity },
+    { apply idp_con }
+  end
+
+end trunc
+
+namespace is_equiv
+
+  definition inv_homotopy_inv {A B : Type} {f g : A → B} [is_equiv f] [is_equiv g] (p : f ~ g)
+    : f⁻¹ ~ g⁻¹ :=
+  λb, (left_inv g (f⁻¹ b))⁻¹ ⬝ ap g⁻¹ ((p (f⁻¹ b))⁻¹ ⬝ right_inv f b)
+
+  definition to_inv_homotopy_to_inv {A B : Type} {f g : A ≃ B} (p : f ~ g) : f⁻¹ᵉ ~ g⁻¹ᵉ :=
+  inv_homotopy_inv p
+
+end is_equiv
+
+namespace prod
+
+  open prod.ops
+  definition prod_pathover_equiv {A : Type} {B C : A → Type} {a a' : A} (p : a = a')
+    (x : B a × C a) (x' : B a' × C a') : x =[p] x' ≃ x.1 =[p] x'.1 × x.2 =[p] x'.2 :=
+  begin
+    fapply equiv.MK,
+    { intro q, induction q, constructor: constructor },
+    { intro v, induction v with q r, exact prod_pathover _ _ _ q r },
+    { intro v, induction v with q r, induction x with b c, induction x' with b' c',
+      esimp at *, induction q, refine idp_rec_on r _, reflexivity },
+    { intro q, induction q, induction x with b c, reflexivity }
+  end
+
+end prod open prod
+
+namespace sigma
+
+  -- set_option pp.notation false
+  -- set_option pp.binder_types true
+
+  open sigma.ops
+  definition pathover_pr1 [unfold 9] {A : Type} {B : A → Type} {C : Πa, B a → Type}
+    {a a' : A} {p : a = a'} {x : Σb, C a b} {x' : Σb', C a' b'}
+    (q : x =[p] x') : x.1 =[p] x'.1 :=
+  begin induction q, constructor end
+
+  definition is_prop_elimo_self {A : Type} (B : A → Type) {a : A} (b : B a) {H : is_prop (B a)} :
+    @is_prop.elimo A B a a idp b b H = idpo :=
+  !is_prop.elim
+
+  definition sigma_pathover_equiv_of_is_prop {A : Type} {B : A → Type} (C : Πa, B a → Type)
+    {a a' : A} (p : a = a') (x : Σb, C a b) (x' : Σb', C a' b')
+    [Πa b, is_prop (C a b)] : x =[p] x' ≃ x.1 =[p] x'.1 :=
+  begin
+    fapply equiv.MK,
+    { exact pathover_pr1 },
+    { intro q, induction x with b c, induction x' with b' c', esimp at q, induction q,
+      apply pathover_idp_of_eq, exact sigma_eq idp !is_prop.elimo },
+    { intro q, induction x with b c, induction x' with b' c', esimp at q, induction q,
+      have c = c', from !is_prop.elim, induction this,
+      rewrite [▸*, is_prop_elimo_self (C a) c] },
+    { intro q, induction q, induction x with b c, rewrite [▸*, is_prop_elimo_self (C a) c] }
+  end
+
+  definition sigma_ua {A B : Type} (C : A ≃ B → Type) :
+    (Σ(p : A = B), C (equiv_of_eq p)) ≃ Σ(e : A ≃ B), C e :=
+  sigma_equiv_sigma_left' !eq_equiv_equiv
+
+  -- definition sigma_pathover_equiv_of_is_prop {A : Type} {B : A → Type} {C : Πa, B a → Type}
+  --   {a a' : A} {p : a = a'} {b : B a} {b' : B a'} {c : C a b} {c' : C a' b'}
+  --   [Πa b, is_prop (C a b)] : ⟨b, c⟩ =[p] ⟨b', c'⟩ ≃ b =[p] b' :=
+  -- begin
+  --   fapply equiv.MK,
+  --   { exact pathover_pr1 },
+  --   { intro q, induction q, apply pathover_idp_of_eq, exact sigma_eq idp !is_prop.elimo },
+  --   { intro q, induction q,
+  --     have c = c', from !is_prop.elim, induction this,
+  --     rewrite [▸*, is_prop_elimo_self (C a) c] },
+  --   { esimp, generalize ⟨b, c⟩, intro x q, }
+  -- end
+--rexact @(ap pathover_pr1) _ idpo _,
+
+end sigma open sigma
+
 namespace group
   open is_trunc
 
+  definition to_fun_isomorphism_trans {G H K : Group} (φ : G ≃g H) (ψ : H ≃g K) :
+    φ ⬝g ψ ~ ψ ∘ φ :=
+  by reflexivity
+
+  definition pmap_of_homomorphism_gid (G : Group) : pmap_of_homomorphism (gid G) ~* pid G :=
+  begin
+    fapply phomotopy_of_homotopy, reflexivity
+  end
+
+  definition pmap_of_homomorphism_gcompose {G H K : Group} (ψ : H →g K) (φ : G →g H)
+    : pmap_of_homomorphism (ψ ∘g φ) ~* pmap_of_homomorphism ψ ∘* pmap_of_homomorphism φ :=
+  begin
+    fapply phomotopy_of_homotopy, reflexivity
+  end
+
+  definition pmap_of_homomorphism_phomotopy {G H : Group} {φ ψ : G →g H} (H : φ ~ ψ)
+    : pmap_of_homomorphism φ ~* pmap_of_homomorphism ψ :=
+  begin
+    fapply phomotopy_of_homotopy, exact H
+  end
+
+  definition pequiv_of_isomorphism_trans {G₁ G₂ G₃ : Group} (φ : G₁ ≃g G₂) (ψ : G₂ ≃g G₂) :
+    pequiv_of_isomorphism (φ ⬝g ψ) ~* pequiv_of_isomorphism ψ ∘* pequiv_of_isomorphism φ :=
+  begin
+    apply phomotopy_of_homotopy, reflexivity
+  end
+
+  definition isomorphism_eq {G H : Group} {φ ψ : G ≃g H} (p : φ ~ ψ) : φ = ψ :=
+  begin
+    induction φ with φ φe, induction ψ with ψ ψe,
+    exact apd011 isomorphism.mk (homomorphism_eq p) !is_prop.elimo
+  end
+
+  definition is_set_isomorphism [instance] (G H : Group) : is_set (G ≃g H) :=
+  begin
+    have H : G ≃g H ≃ Σ(f : G →g H), is_equiv f,
+    begin
+      fapply equiv.MK,
+      { intro φ, induction φ, constructor, assumption },
+      { intro v, induction v, constructor, assumption },
+      { intro v, induction v, reflexivity },
+      { intro φ, induction φ, reflexivity }
+    end,
+    apply is_trunc_equiv_closed_rev, exact H
+  end
+
+
+--  definition is_equiv_isomorphism
+
+
   -- some extra instances for type class inference
   -- definition is_homomorphism_comm_homomorphism [instance] {G G' : AbGroup} (φ : G →g G')
   --   : @is_homomorphism G G' (@ab_group.to_group _ (AbGroup.struct G))
@@ -28,6 +320,18 @@ end group open group
 
 namespace pi -- move to types.arrow
 
+  definition pmap_eq_equiv {X Y : Type*} (f g : X →* Y) : (f = g) ≃ (f ~* g) :=
+  begin
+    refine eq_equiv_fn_eq_of_equiv (@pmap.sigma_char X Y) f g ⬝e _,
+    refine !sigma_eq_equiv ⬝e _,
+    refine _ ⬝e (phomotopy.sigma_char f g)⁻¹ᵉ,
+    fapply sigma_equiv_sigma,
+    { esimp, apply eq_equiv_homotopy },
+    { induction g with g gp, induction Y with Y y0, esimp, intro p, induction p, esimp at *,
+      refine !pathover_idp ⬝e _, refine _ ⬝e !eq_equiv_eq_symm,
+      apply equiv_eq_closed_right, exact !idp_con⁻¹ }
+  end
+
   definition pmap_eq_idp {X Y : Type*} (f : X →* Y) :
     pmap_eq (λx, idpath (f x)) !idp_con⁻¹ = idpath f :=
   begin
@@ -57,28 +361,38 @@ end pi open pi
 
 namespace eq
 
+  infix ` ⬝hty `:75 := homotopy.trans
+  postfix `⁻¹ʰᵗʸ`:(max+1) := homotopy.symm
+
+  definition hassoc {A B C D : Type} (h : C → D) (g : B → C) (f : A → B) : (h ∘ g) ∘ f ~ h ∘ (g ∘ f) :=
+  λa, idp
+
+  -- to algebra.homotopy_group
+  definition homotopy_group_homomorphism_pcompose (n : ℕ) [H : is_succ n] {A B C : Type*} (g : B →* C)
+    (f : A →* B) : π→g[n] (g ∘* f) ~ π→g[n] g ∘ π→g[n] f :=
+  begin
+    induction H with n, exact to_homotopy (homotopy_group_functor_compose (succ n) g f)
+  end
+
+  definition apn_pinv (n : ℕ) {A B : Type*} (f : A ≃* B) :
+    Ω→[n] f⁻¹ᵉ* ~* (loopn_pequiv_loopn n f)⁻¹ᵉ* :=
+  begin
+    refine !to_pinv_pequiv_MK2⁻¹*
+  end
+
+  -- definition homotopy_group_homomorphism_pinv (n : ℕ) {A B : Type*} (f : A ≃* B) :
+  --   π→g[n+1] f⁻¹ᵉ* ~ (homotopy_group_isomorphism_of_pequiv n f)⁻¹ᵍ :=
+  -- begin
+  --   -- refine ptrunc_functor_phomotopy 0 !apn_pinv ⬝hty _,
+  --   -- intro x, esimp,
+  -- end
+
   -- definition natural_square_tr_eq {A B : Type} {a a' : A} {f g : A → B}
   --   (p : f ~ g) (q : a = a') : natural_square p q = square_of_pathover (apd p q) :=
   -- idp
 
 end eq open eq
 
-namespace pointed
-
-  -- /- the pointed type of (unpointed) dependent maps -/
-  -- definition pupi [constructor] {A : Type} (P : A → Type*) : Type* :=
-  -- pointed.mk' (Πa, P a)
-
-  -- definition loop_pupi_commute {A : Type} (B : A → Type*) : Ω(pupi B) ≃* pupi (λa, Ω (B a)) :=
-  -- pequiv_of_equiv eq_equiv_homotopy rfl
-
-  -- definition equiv_pupi_right {A : Type} {P Q : A → Type*} (g : Πa, P a ≃* Q a)
-  --   : pupi P ≃* pupi Q :=
-  -- pequiv_of_equiv (pi_equiv_pi_right g)
-  --   begin esimp, apply eq_of_homotopy, intros a, esimp, exact (respect_pt (g a)) end
-
-end pointed open pointed
-
 namespace fiber
 
 
@@ -95,6 +409,46 @@ namespace fiber
 
 end fiber
 
+namespace is_conn
+
+  open unit trunc_index nat is_trunc pointed.ops
+
+  definition is_contr_of_trivial_homotopy' (n : ℕ₋₂) (A : Type) [is_trunc n A] [is_conn -1 A]
+    (H : Πk a, is_contr (π[k] (pointed.MK A a))) : is_contr A :=
+  begin
+    assert aa : trunc -1 A,
+    { apply center },
+    assert H3 : is_conn 0 A,
+    { induction aa with a, exact H 0 a },
+    exact is_contr_of_trivial_homotopy n A H
+  end
+
+  -- don't make is_prop_is_trunc an instance
+  definition is_trunc_succ_is_trunc [instance] (n m : ℕ₋₂) (A : Type) : is_trunc (n.+1) (is_trunc m A) :=
+  is_trunc_of_le _ !minus_one_le_succ
+
+  definition is_conn_of_trivial_homotopy (n : ℕ₋₂) (m : ℕ) (A : Type) [is_trunc n A] [is_conn 0 A]
+    (H : Π(k : ℕ) a, k ≤ m → is_contr (π[k] (pointed.MK A a))) : is_conn m A :=
+  begin
+    apply is_contr_of_trivial_homotopy_nat m (trunc m A),
+    intro k a H2,
+    induction a with a,
+    apply is_trunc_equiv_closed_rev,
+      exact equiv_of_pequiv (homotopy_group_trunc_of_le (pointed.MK A a) _ _ H2),
+    exact H k a H2
+  end
+
+  definition is_conn_of_trivial_homotopy_pointed (n : ℕ₋₂) (m : ℕ) (A : Type*) [is_trunc n A]
+    (H : Π(k : ℕ), k ≤ m → is_contr (π[k] A)) : is_conn m A :=
+  begin
+    have is_conn 0 A, proof H 0 !zero_le qed,
+    apply is_conn_of_trivial_homotopy n m A,
+    intro k a H2, revert a, apply is_conn.elim -1,
+    cases A with A a, exact H k H2
+  end
+
+end is_conn
+
 namespace circle
 
 
@@ -117,6 +471,262 @@ namespace circle
 
 end circle
 
+namespace susp
+
+  definition psusp_functor_phomotopy {A B : Type*} {f g : A →* B} (p : f ~* g) :
+    psusp_functor f ~* psusp_functor g :=
+  begin
+    fapply phomotopy.mk,
+    { intro x, induction x,
+      { reflexivity },
+      { reflexivity },
+      { apply eq_pathover, apply hdeg_square, esimp, refine !elim_merid ⬝ _ ⬝ !elim_merid⁻¹ᵖ,
+        exact ap merid (p a), }},
+    { reflexivity },
+  end
+
+  definition psusp_functor_pid (A : Type*) : psusp_functor (pid A) ~* pid (psusp A) :=
+  begin
+    fapply phomotopy.mk,
+    { intro x, induction x,
+      { reflexivity },
+      { reflexivity },
+      { apply eq_pathover_id_right, apply hdeg_square, apply elim_merid }},
+    { reflexivity },
+  end
+
+  definition psusp_functor_pcompose {A B C : Type*} (g : B →* C) (f : A →* B) :
+    psusp_functor (g ∘* f) ~* psusp_functor g ∘* psusp_functor f :=
+  begin
+    fapply phomotopy.mk,
+    { intro x, induction x,
+      { reflexivity },
+      { reflexivity },
+      { apply eq_pathover, apply hdeg_square, esimp,
+        refine !elim_merid ⬝ _ ⬝ (ap_compose (psusp_functor g) _ _)⁻¹ᵖ,
+        refine _ ⬝ ap02 _ !elim_merid⁻¹, exact !elim_merid⁻¹ }},
+    { reflexivity },
+  end
+
+  definition psusp_elim_psusp_functor {A B C : Type*} (g : B →* Ω C) (f : A →* B) :
+    psusp.elim g ∘* psusp_functor f ~* psusp.elim (g ∘* f) :=
+  begin
+    refine !passoc ⬝* _, exact pwhisker_left _ !psusp_functor_pcompose⁻¹*
+  end
+
+  definition psusp_elim_phomotopy {A B : Type*} {f g : A →* Ω B} (p : f ~* g) : psusp.elim f ~* psusp.elim g :=
+  pwhisker_left _ (psusp_functor_phomotopy p)
+
+  definition psusp_elim_natural {X Y Z : Type*} (g : Y →* Z) (f : X →* Ω Y)
+    : g ∘* psusp.elim f ~* psusp.elim (Ω→ g ∘* f) :=
+  begin
+    refine _ ⬝* pwhisker_left _ !psusp_functor_pcompose⁻¹*,
+    refine !passoc⁻¹* ⬝* _ ⬝* !passoc,
+    exact pwhisker_right _ !loop_psusp_counit_natural
+  end
+
+end susp
+
+namespace category
+
+  -- replace precategory_group with precategory_Group (the former has a universe error)
+  definition precategory_Group.{u} [instance] [constructor] : precategory.{u+1 u} Group :=
+  begin
+    fapply precategory.mk,
+    { exact λG H, G →g H },
+    { exact _ },
+    { exact λG H K ψ φ, ψ ∘g φ },
+    { exact λG, gid G },
+    { intros, apply homomorphism_eq, esimp },
+    { intros, apply homomorphism_eq, esimp },
+    { intros, apply homomorphism_eq, esimp }
+  end
+
+
+  definition precategory_AbGroup.{u} [instance] [constructor] : precategory.{u+1 u} AbGroup :=
+  begin
+    fapply precategory.mk,
+    { exact λG H, G →g H },
+    { exact _ },
+    { exact λG H K ψ φ, ψ ∘g φ },
+    { exact λG, gid G },
+    { intros, apply homomorphism_eq, esimp },
+    { intros, apply homomorphism_eq, esimp },
+    { intros, apply homomorphism_eq, esimp }
+  end
+  open iso
+  definition Group_is_iso_of_is_equiv {G H : Group} (φ : G →g H) (H : is_equiv (group_fun φ)) :
+    is_iso φ :=
+  begin
+    fconstructor,
+    { exact (isomorphism.mk φ H)⁻¹ᵍ },
+    { apply homomorphism_eq, rexact left_inv φ },
+    { apply homomorphism_eq, rexact right_inv φ }
+  end
+
+  definition Group_is_equiv_of_is_iso {G H : Group} (φ : G ⟶ H) (Hφ : is_iso φ) :
+    is_equiv (group_fun φ) :=
+  begin
+    fapply adjointify,
+    { exact group_fun φ⁻¹ʰ },
+    { note p := right_inverse φ, exact ap010 group_fun p },
+    { note p := left_inverse φ,  exact ap010 group_fun p }
+  end
+
+  definition Group_iso_equiv (G H : Group) : (G ≅ H) ≃ (G ≃g H) :=
+  begin
+    fapply equiv.MK,
+    { intro φ, induction φ with φ φi, constructor, exact Group_is_equiv_of_is_iso φ _ },
+    { intro v, induction v with φ φe, constructor, exact Group_is_iso_of_is_equiv φ _ },
+    { intro v, induction v with φ φe, apply isomorphism_eq, reflexivity },
+    { intro φ, induction φ with φ φi, apply iso_eq, reflexivity }
+  end
+
+  definition Group_props.{u} {A : Type.{u}} (v : (A → A → A) × (A → A) × A) : Prop.{u} :=
+  begin
+    induction v with m v, induction v with i o,
+    fapply trunctype.mk,
+    { exact is_set A × (Πa, m a o = a) × (Πa, m o a = a) × (Πa b c, m (m a b) c = m a (m b c)) ×
+      (Πa, m (i a) a = o) },
+    { apply is_trunc_of_imp_is_trunc, intro v, induction v with H v,
+      have is_prop (Πa, m a o = a), from _,
+      have is_prop (Πa, m o a = a), from _,
+      have is_prop (Πa b c, m (m a b) c = m a (m b c)), from _,
+      have is_prop (Πa, m (i a) a = o), from _,
+      apply is_trunc_prod }
+  end
+
+  definition Group.sigma_char2.{u} : Group.{u} ≃
+    Σ(A : Type.{u}) (v : (A → A → A) × (A → A) × A), Group_props v :=
+  begin
+    fapply equiv.MK,
+    { intro G, refine ⟨G, _⟩, induction G with G g, induction g with m s ma o om mo i mi,
+      repeat (fconstructor; do 2 try assumption), },
+    { intro v, induction v with x v, induction v with y v, repeat induction y with x y,
+      repeat induction v with x v, constructor, fconstructor, repeat assumption },
+    { intro v, induction v with x v, induction v with y v, repeat induction y with x y,
+      repeat induction v with x v, reflexivity },
+    { intro v, repeat induction v with x v, reflexivity },
+  end
+  open is_trunc
+
+  section
+  local attribute group.to_has_mul group.to_has_inv [coercion]
+
+  theorem inv_eq_of_mul_eq {A : Type} (G H : group A) (p : @mul A G ~2 @mul A H) :
+    @inv A G ~ @inv A H :=
+  begin
+    have foo : Π(g : A), @inv A G g = (@inv A G g * g) * @inv A H g,
+      from λg, !mul_inv_cancel_right⁻¹,
+    cases G with Gm Gs Gh1 G1 Gh2 Gh3 Gi Gh4,
+    cases H with Hm Hs Hh1 H1 Hh2 Hh3 Hi Hh4,
+    change Gi ~ Hi, intro g, have p' : Gm ~2 Hm, from p,
+    calc
+      Gi g = Hm (Hm (Gi g) g) (Hi g) : foo
+       ... = Hm (Gm (Gi g) g) (Hi g) : by rewrite p'
+       ... = Hm G1 (Hi g) : by rewrite Gh4
+       ... = Gm G1 (Hi g) : by rewrite p'
+       ... = Hi g : Gh2
+  end
+
+  theorem one_eq_of_mul_eq {A : Type} (G H : group A)
+    (p : @mul A (group.to_has_mul G) ~2 @mul A (group.to_has_mul H)) :
+    @one A (group.to_has_one G) = @one A (group.to_has_one H) :=
+  begin
+    cases G with Gm Gs Gh1 G1 Gh2 Gh3 Gi Gh4,
+    cases H with Hm Hs Hh1 H1 Hh2 Hh3 Hi Hh4,
+    exact (Hh2 G1)⁻¹ ⬝ (p H1 G1)⁻¹ ⬝ Gh3 H1,
+  end
+  end
+
+  open prod.ops
+  definition group_of_Group_props.{u} {A : Type.{u}} {m : A → A → A} {i : A → A} {o : A}
+    (H : Group_props (m, (i, o))) : group A :=
+  ⦃group, mul := m, inv := i, one := o, is_set_carrier := H.1,
+    mul_one := H.2.1, one_mul := H.2.2.1, mul_assoc := H.2.2.2.1, mul_left_inv := H.2.2.2.2⦄
+
+  theorem Group_eq_equiv_lemma2 {A : Type} {m m' : A → A → A} {i i' : A → A} {o o' : A}
+    (H : Group_props (m, (i, o))) (H' : Group_props (m', (i', o'))) :
+    (m, (i, o)) = (m', (i', o')) ≃ (m ~2 m') :=
+  begin
+    have is_set A, from pr1 H,
+    apply equiv_of_is_prop,
+    { intro p, exact apd100 (eq_pr1 p)},
+    { intro p, apply prod_eq (eq_of_homotopy2 p),
+      apply prod_eq: esimp [Group_props] at *; esimp,
+      { apply eq_of_homotopy,
+        exact inv_eq_of_mul_eq (group_of_Group_props H) (group_of_Group_props H') p },
+      { exact one_eq_of_mul_eq (group_of_Group_props H) (group_of_Group_props H') p }}
+  end
+
+  open sigma.ops
+
+  theorem Group_eq_equiv_lemma {G H : Group}
+    (p : (Group.sigma_char2 G).1 = (Group.sigma_char2 H).1) :
+    ((Group.sigma_char2 G).2 =[p] (Group.sigma_char2 H).2) ≃
+    (is_homomorphism (equiv_of_eq (proof p qed : Group.carrier G = Group.carrier H))) :=
+  begin
+    refine !sigma_pathover_equiv_of_is_prop ⬝e _,
+    induction G with G g, induction H with H h,
+    esimp [Group.sigma_char2] at p, induction p,
+    refine !pathover_idp ⬝e _,
+    induction g with m s ma o om mo i mi, induction h with μ σ μa ε εμ με ι μι,
+    exact Group_eq_equiv_lemma2 (Group.sigma_char2 (Group.mk G (group.mk m s ma o om mo i mi))).2.2
+                                (Group.sigma_char2 (Group.mk G (group.mk μ σ μa ε εμ με ι μι))).2.2
+  end
+
+  definition isomorphism.sigma_char (G H : Group) : (G ≃g H) ≃ Σ(e : G ≃ H), is_homomorphism e :=
+  begin
+    fapply equiv.MK,
+    { intro φ, exact ⟨equiv_of_isomorphism φ, to_respect_mul φ⟩ },
+    { intro v, induction v with e p, exact isomorphism_of_equiv e p },
+    { intro v, induction v with e p, induction e, reflexivity },
+    { intro φ, induction φ with φ H, induction φ, reflexivity },
+  end
+
+  definition Group_eq_equiv (G H : Group) : G = H ≃ (G ≃g H) :=
+  begin
+    refine (eq_equiv_fn_eq_of_equiv Group.sigma_char2 G H) ⬝e _,
+    refine !sigma_eq_equiv ⬝e _,
+    refine sigma_equiv_sigma_right Group_eq_equiv_lemma ⬝e _,
+    transitivity (Σ(e : (Group.sigma_char2 G).1 ≃ (Group.sigma_char2 H).1),
+      @is_homomorphism _ _ _ _ (to_fun e)), apply sigma_ua,
+    exact !isomorphism.sigma_char⁻¹ᵉ
+  end
+
+  definition to_fun_Group_eq_equiv {G H : Group} (p : G = H)
+    : Group_eq_equiv G H p ~ isomorphism_of_eq p :=
+  begin
+    induction p, reflexivity
+  end
+
+  definition Group_eq2 {G H : Group} {p q : G = H}
+    (r : isomorphism_of_eq p ~ isomorphism_of_eq q) : p = q :=
+  begin
+    apply eq_of_fn_eq_fn (Group_eq_equiv G H),
+    apply isomorphism_eq,
+    intro g, refine to_fun_Group_eq_equiv p g ⬝ r g ⬝ (to_fun_Group_eq_equiv q g)⁻¹,
+  end
+
+  definition Group_eq_equiv_Group_iso (G₁ G₂ : Group) : G₁ = G₂ ≃ G₁ ≅ G₂ :=
+  Group_eq_equiv G₁ G₂ ⬝e (Group_iso_equiv G₁ G₂)⁻¹ᵉ
+
+  definition category_Group.{u} : category Group.{u} :=
+  category.mk precategory_Group
+  begin
+    intro G H,
+    apply is_equiv_of_equiv_of_homotopy (Group_eq_equiv_Group_iso G H),
+    intro p, induction p, fapply iso_eq, apply homomorphism_eq, reflexivity
+  end
+
+  definition category_AbGroup : category AbGroup :=
+  category.mk precategory_AbGroup sorry
+
+  definition Grp.{u} [constructor] : Category := category.Mk Group.{u} category_Group
+  definition AbGrp [constructor] : Category := category.Mk AbGroup category_AbGroup
+
+end category
+
 namespace sphere
 
   -- definition constant_sphere_map_sphere {n m : ℕ} (H : n < m) (f : S* n →* S* m) :
@@ -131,7 +741,7 @@ namespace sphere
 
 end sphere
 
-definition image_pathover {A B : Type} (f : A → B) {x y : B} (p : x = y) (u : image f x) (v : image f y) : u =[p] v := 
+definition image_pathover {A B : Type} (f : A → B) {x y : B} (p : x = y) (u : image f x) (v : image f y) : u =[p] v :=
   begin
     apply is_prop.elimo
   end
@@ -149,7 +759,7 @@ definition is_embedding_factor : is_embedding h → is_embedding f :=
     fapply is_embedding_of_is_injective,
     intro x y p,
     fapply @is_injective_of_is_embedding _ _ _ E _ _ (ap g p)
-  end 
+  end
 
 definition is_surjective_factor : is_surjective h → is_surjective g :=
   begin