diff --git a/algebra/quotient_group.hlean b/algebra/quotient_group.hlean
new file mode 100644
index 0000000..575b479
--- /dev/null
+++ b/algebra/quotient_group.hlean
@@ -0,0 +1,737 @@
+/-
+Copyright (c) 2015 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn, Egbert Rijke, Jeremy Avigad
+
+Constructions with groups
+-/
+
+import hit.set_quotient .subgroup ..move_to_lib types.equiv
+
+open eq algebra is_trunc set_quotient relation sigma sigma.ops prod trunc function equiv is_equiv
+open property
+
+namespace group
+  variables {G G' : Group}
+            (H : property G) [is_subgroup G H]
+            (N : property G) [is_normal_subgroup G N]
+            {g g' h h' k : G}
+            (N' : property G') [is_normal_subgroup G' N']
+  variables {A B : AbGroup}
+
+  /- Quotient Group -/
+
+  definition homotopy_of_homomorphism_eq {f g : G →g G'}(p : f = g) : f ~ g :=
+  λx : G , ap010 group_fun p x
+
+  definition quotient_rel [constructor] (g h : G) : Prop := g * h⁻¹ ∈ N
+
+  variable {N}
+
+    -- We prove that quotient_rel is an equivalence relation
+  theorem quotient_rel_refl (g : G) : quotient_rel N g g :=
+  transport (λx, N x) !mul.right_inv⁻¹ (subgroup_one_mem N)
+
+  theorem quotient_rel_symm (r : quotient_rel N g h) : quotient_rel N h g :=
+  transport (λx, N x) (!mul_inv ⬝ ap (λx, x * _) !inv_inv)
+    begin apply subgroup_inv_mem r end
+
+  theorem quotient_rel_trans (r : quotient_rel N g h) (s : quotient_rel N h k)
+    : quotient_rel N g k :=
+  have H1 : N ((g * h⁻¹) * (h * k⁻¹)), from subgroup_mul_mem r s,
+  have H2 : (g * h⁻¹) * (h * k⁻¹) = g * k⁻¹, from calc
+    (g * h⁻¹) * (h * k⁻¹) = ((g * h⁻¹) * h) * k⁻¹ : by rewrite [mul.assoc (g * h⁻¹)]
+                      ... = g * k⁻¹               : by rewrite inv_mul_cancel_right,
+  show N (g * k⁻¹), by rewrite [-H2]; exact H1
+
+  theorem is_equivalence_quotient_rel : is_equivalence (quotient_rel N) :=
+  is_equivalence.mk quotient_rel_refl
+                    (λg h, quotient_rel_symm)
+                    (λg h k, quotient_rel_trans)
+
+    -- We prove that quotient_rel respects inverses and multiplication, so
+    -- it is a congruence relation
+  theorem quotient_rel_resp_inv (r : quotient_rel N g h) : quotient_rel N g⁻¹ h⁻¹ :=
+  have H1 : g⁻¹ * (h * g⁻¹) * g ∈ N, from
+    is_normal_subgroup' g (quotient_rel_symm r),
+  have H2 : g⁻¹ * (h * g⁻¹) * g = g⁻¹ * h⁻¹⁻¹, from calc
+    g⁻¹ * (h * g⁻¹) * g = g⁻¹ * h * g⁻¹ * g : by rewrite -mul.assoc
+                    ... = g⁻¹ * h           : inv_mul_cancel_right
+                    ... = g⁻¹ * h⁻¹⁻¹       : by rewrite algebra.inv_inv,
+  show g⁻¹ * h⁻¹⁻¹ ∈ N, by rewrite [-H2]; exact H1
+
+  theorem quotient_rel_resp_mul (r : quotient_rel N g h) (r' : quotient_rel N g' h')
+    : quotient_rel N (g * g') (h * h') :=
+  have H1 : g * ((g' * h'⁻¹) * h⁻¹) ∈ N, from
+    normal_subgroup_insert r' r,
+  have H2 : g * ((g' * h'⁻¹) * h⁻¹) = (g * g') * (h * h')⁻¹, from calc
+    g * ((g' * h'⁻¹) * h⁻¹) = g * (g' * (h'⁻¹ * h⁻¹)) : by rewrite [mul.assoc]
+                        ... = (g * g') * (h'⁻¹ * h⁻¹) : mul.assoc
+                        ... = (g * g') * (h * h')⁻¹ : by rewrite [mul_inv],
+  show N ((g * g') * (h * h')⁻¹), from transport (λx, N x) H2 H1
+
+  local attribute is_equivalence_quotient_rel [instance]
+
+  variable (N)
+
+  definition qg : Type := set_quotient (quotient_rel N)
+
+  variable {N}
+
+  local attribute qg [reducible]
+
+  definition quotient_one [constructor] : qg N := class_of one
+  definition quotient_inv [unfold 3] : qg N → qg N :=
+  quotient_unary_map has_inv.inv (λg g' r, quotient_rel_resp_inv r)
+  definition quotient_mul [unfold 3 4] : qg N → qg N → qg N :=
+  quotient_binary_map has_mul.mul (λg g' r h h' r', quotient_rel_resp_mul r r')
+
+  section
+  local notation 1 := quotient_one
+  local postfix ⁻¹ := quotient_inv
+  local infix * := quotient_mul
+
+  theorem quotient_mul_assoc (g₁ g₂ g₃ : qg N) : g₁ * g₂ * g₃ = g₁ * (g₂ * g₃) :=
+  begin
+    refine set_quotient.rec_prop _ g₁,
+    refine set_quotient.rec_prop _ g₂,
+    refine set_quotient.rec_prop _ g₃,
+    clear g₁ g₂ g₃, intro g₁ g₂ g₃,
+    exact ap class_of !mul.assoc
+  end
+
+  theorem quotient_one_mul (g : qg N) : 1 * g = g :=
+  begin
+    refine set_quotient.rec_prop _ g, clear g, intro g,
+    exact ap class_of !one_mul
+  end
+
+  theorem quotient_mul_one (g : qg N) : g * 1 = g :=
+  begin
+    refine set_quotient.rec_prop _ g, clear g, intro g,
+    exact ap class_of !mul_one
+  end
+
+  theorem quotient_mul_left_inv (g : qg N) : g⁻¹ * g = 1 :=
+  begin
+    refine set_quotient.rec_prop _ g, clear g, intro g,
+    exact ap class_of !mul.left_inv
+  end
+
+  theorem quotient_mul_comm {G : AbGroup} {N : property G} [is_normal_subgroup G N] (g h : qg N)
+    : g * h = h * g :=
+  begin
+    refine set_quotient.rec_prop _ g, clear g, intro g,
+    refine set_quotient.rec_prop _ h, clear h, intro h,
+    apply ap class_of, esimp, apply mul.comm
+  end
+
+  end
+
+  variable (N)
+  definition group_qg [constructor] : group (qg N) :=
+  group.mk _ quotient_mul quotient_mul_assoc quotient_one quotient_one_mul quotient_mul_one
+           quotient_inv quotient_mul_left_inv
+
+  definition quotient_group [constructor] : Group :=
+  Group.mk _ (group_qg N)
+
+  definition ab_group_qg [constructor] {G : AbGroup} (N : property G) [is_normal_subgroup G N]
+    : ab_group (qg N) :=
+  ⦃ab_group, group_qg N, mul_comm := quotient_mul_comm⦄
+
+  definition quotient_ab_group [constructor] {G : AbGroup} (N : property G) [is_subgroup G N]
+    : AbGroup :=
+  AbGroup.mk _ (@ab_group_qg G N (is_normal_subgroup_ab _))
+
+  definition qg_map [constructor] : G →g quotient_group N :=
+  homomorphism.mk class_of (λ g h, idp)
+
+  definition ab_qg_map {G : AbGroup} (N : property G) [is_subgroup G N] : G →g quotient_ab_group N :=
+  @qg_map _ N (is_normal_subgroup_ab _)
+
+ definition is_surjective_ab_qg_map {A : AbGroup} (N : property A) [is_subgroup A N] : is_surjective (ab_qg_map N) :=
+  begin
+    intro x, induction x,
+    fapply image.mk,
+    exact a, reflexivity,
+    apply is_prop.elimo
+  end
+
+  namespace quotient
+    notation `⟦`:max a `⟧`:0 := qg_map _ a
+  end quotient
+
+  open quotient
+  variables {N N'}
+
+  definition qg_map_eq_one (g : G) (H : N g) : qg_map N g = 1 :=
+  begin
+    apply eq_of_rel,
+      have e : (g * 1⁻¹ = g),
+      from calc
+      g * 1⁻¹ = g * 1 : one_inv
+        ...   = g : mul_one,
+    unfold quotient_rel, rewrite e, exact H
+  end
+
+  definition ab_qg_map_eq_one {K : property A} [is_subgroup A K] (g :A) (H : K g) : ab_qg_map K g = 1 :=
+  begin
+    apply eq_of_rel,
+      have e : (g * 1⁻¹ = g),
+      from calc
+      g * 1⁻¹ = g * 1 : one_inv
+        ...   = g : mul_one,
+    unfold quotient_rel, xrewrite e, exact H
+  end
+
+   --- there should be a smarter way to do this!! Please have a look, Floris.
+  definition rel_of_qg_map_eq_one (g : G) (H : qg_map N g = 1) : g ∈ N :=
+  begin
+    have e : (g * 1⁻¹ = g),
+    from calc
+      g * 1⁻¹ = g * 1 : one_inv
+        ...   = g : mul_one,
+    rewrite (inverse e),
+    apply rel_of_eq _ H
+  end
+
+  definition rel_of_ab_qg_map_eq_one {K : property A} [is_subgroup A K] (a :A) (H : ab_qg_map K a = 1) : a ∈ K :=
+  begin
+    have e : (a * 1⁻¹ = a),
+    from calc
+      a * 1⁻¹ = a * 1 : one_inv
+        ...   = a : mul_one,
+    rewrite (inverse e),
+    have is_normal_subgroup A K, from is_normal_subgroup_ab _,
+    apply rel_of_eq (quotient_rel K) H
+  end
+
+  definition quotient_group_elim_fun [unfold 6] (f : G →g G') (H : Π⦃g⦄, N g → f g = 1)
+    (g : quotient_group N) : G' :=
+  begin
+    refine set_quotient.elim f _ g,
+    intro g h K,
+    apply eq_of_mul_inv_eq_one,
+    have e : f (g * h⁻¹) = f g * (f h)⁻¹,
+    from calc
+      f (g * h⁻¹) = f g * (f h⁻¹) : to_respect_mul
+             ...  = f g * (f h)⁻¹ : to_respect_inv,
+    rewrite (inverse e),
+    apply H, exact K
+  end
+
+  definition quotient_group_elim [constructor] (f : G →g G') (H : Π⦃g⦄, g ∈ N → f g = 1) : quotient_group N →g G' :=
+  begin
+    fapply homomorphism.mk,
+      -- define function
+    { exact quotient_group_elim_fun f H },
+    { intro g h, induction g using set_quotient.rec_prop with g,
+      induction h using set_quotient.rec_prop with h,
+      krewrite (inverse (to_respect_mul (qg_map N) g h)),
+      unfold qg_map, esimp, exact to_respect_mul f g h }
+  end
+
+  example {K : property A} [is_subgroup A K] :
+    quotient_ab_group K = @quotient_group A K (is_normal_subgroup_ab _) := rfl
+
+  definition quotient_ab_group_elim [constructor] {K : property A} [is_subgroup A K] (f : A →g B)
+    (H : Π⦃g⦄, g ∈ K → f g = 1) : quotient_ab_group K →g B :=
+  @quotient_group_elim A B K (is_normal_subgroup_ab _) f H
+
+  definition quotient_group_compute (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) (g : G) :
+    quotient_group_elim f H (qg_map N g) = f g :=
+  begin
+    reflexivity
+  end
+
+  definition gelim_unique (f : G →g G') (H : Π⦃g⦄, g ∈ N → f g = 1) (k : quotient_group N →g G')
+    : ( k ∘g qg_map N ~ f ) → k ~ quotient_group_elim f H :=
+  begin
+    intro K cg, induction cg using set_quotient.rec_prop with g,
+    exact K g
+  end
+
+  definition ab_gelim_unique {K : property A} [is_subgroup A K] (f : A →g B) (H : Π (a :A), a ∈ K → f a = 1) (k : quotient_ab_group K →g B)
+    : ( k ∘g ab_qg_map K ~ f) → k ~ quotient_ab_group_elim f H :=
+--@quotient_group_elim A B K (is_normal_subgroup_ab _) f H :=
+  @gelim_unique _ _ K (is_normal_subgroup_ab _) f H _
+
+  definition qg_universal_property (f : G →g G') (H : Π⦃g⦄, N g → f g = 1)  :
+    is_contr (Σ(g : quotient_group N →g G'), g ∘ qg_map N ~ f) :=
+  begin
+    fapply is_contr.mk,
+      -- give center of contraction
+    { fapply sigma.mk, exact quotient_group_elim f H, exact quotient_group_compute f H },
+      -- give contraction
+    { intro pair, induction pair with g p, fapply sigma_eq,
+      {esimp, apply homomorphism_eq, symmetry, exact gelim_unique f H g p},
+      {fapply is_prop.elimo} }
+  end
+
+  definition ab_qg_universal_property {K : property A} [is_subgroup A K] (f : A →g B) (H : Π (a :A), K a → f a = 1) :
+  is_contr ((Σ(g : quotient_ab_group K →g B), g ∘g ab_qg_map K ~ f) ) :=
+  begin
+    fapply @qg_universal_property _ _ K (is_normal_subgroup_ab _),
+    exact H
+  end
+
+  definition quotient_group_functor_contr {K L : property A} [is_subgroup A K] [is_subgroup A L]
+    (H : Π (a : A), K a → L a) :
+  is_contr ((Σ(g : quotient_ab_group K →g quotient_ab_group L), g ∘g ab_qg_map K ~ ab_qg_map L) ) :=
+  begin
+    fapply ab_qg_universal_property,
+    intro a p,
+    fapply ab_qg_map_eq_one,
+    exact H a p
+  end
+
+  definition quotient_group_functor_id {K : property A} [is_subgroup A K] (H : Π (a : A), K a → K a) :
+    center' (@quotient_group_functor_contr _ K K _ _ H) = ⟨gid (quotient_ab_group K), λ x, rfl⟩ :=
+    begin
+      note p := @quotient_group_functor_contr _ K K _ _ H,
+      fapply eq_of_is_contr,
+    end
+
+  section quotient_group_iso_ua
+
+  set_option pp.universes true
+
+  definition subgroup_rel_eq' {K L : property A} [HK : is_subgroup A K] [HL : is_subgroup A L] (htpy : Π (a : A), K a ≃ L a) : K = L :=
+  begin
+    induction HK with Rone Rmul Rinv, induction HL with Rone' Rmul' Rinv', esimp at *,
+    assert q : K = L,
+    begin
+      fapply eq_of_homotopy,
+      intro a,
+      fapply tua,
+      exact htpy a,
+    end,
+    induction q,
+    assert q : Rone = Rone',
+    begin
+      fapply is_prop.elim,
+    end,
+    induction q,
+    assert q2 : @Rmul = @Rmul',
+    begin
+      fapply is_prop.elim,
+    end,
+    induction q2,
+    assert q : @Rinv = @Rinv',
+    begin
+      fapply is_prop.elim,
+    end,
+    induction q,
+    reflexivity
+  end
+
+  definition subgroup_rel_eq {K L : property A} [is_subgroup A K] [is_subgroup A L] (K_in_L : Π (a : A), a ∈ K → a ∈ L) (L_in_K : Π (a : A), a ∈ L → a ∈ K) : K = L :=
+  begin
+    have htpy : Π (a : A), K a ≃ L a,
+    begin
+      intro a,
+      apply @equiv_of_is_prop (a ∈ K) (a ∈ L) _ _ (K_in_L a) (L_in_K a),
+    end,
+    exact subgroup_rel_eq' htpy,
+  end
+
+  definition  eq_of_ab_qg_group' {K L : property A} [HK : is_subgroup A K] [HL : is_subgroup A L] (p : K = L) : quotient_ab_group K = quotient_ab_group L :=
+  begin
+    revert HK, revert HL, induction p, intros,
+    have HK = HL, begin apply @is_prop.elim _ _ HK HL end,
+    rewrite this
+  end
+
+  definition iso_of_eq {B : AbGroup} (p : A = B) : A ≃g B :=
+  begin
+    induction p, fapply isomorphism.mk, exact gid A, fapply adjointify, exact id, intro a, reflexivity, intro a, reflexivity
+  end
+
+  definition iso_of_ab_qg_group' {K L : property A} [is_subgroup A K] [is_subgroup A L] (p : K = L) : quotient_ab_group K ≃g quotient_ab_group L :=
+  iso_of_eq (eq_of_ab_qg_group' p)
+
+/-
+  definition htpy_of_ab_qg_group' {K L : property A} [HK : is_subgroup A K] [HL : is_subgroup A L] (p : K = L) : (iso_of_ab_qg_group' p) ∘g ab_qg_map K ~ ab_qg_map L :=
+  begin
+    revert HK, revert HL, induction p, intros HK HL, unfold iso_of_ab_qg_group', unfold ab_qg_map
+--    have HK = HL, begin apply @is_prop.elim _ _ HK HL end,
+--    rewrite this
+--    induction p, reflexivity
+  end
+-/
+
+  definition eq_of_ab_qg_group {K L : property A} [is_subgroup A K] [is_subgroup A L] (K_in_L : Π (a : A), K a → L a) (L_in_K : Π (a : A), L a → K a) : quotient_ab_group K = quotient_ab_group L :=
+  eq_of_ab_qg_group' (subgroup_rel_eq K_in_L L_in_K)
+
+  definition iso_of_ab_qg_group {K L : property A} [is_subgroup A K] [is_subgroup A L] (K_in_L : Π (a : A), K a → L a) (L_in_K : Π (a : A), L a → K a) : quotient_ab_group K ≃g quotient_ab_group L :=
+  iso_of_eq (eq_of_ab_qg_group K_in_L L_in_K)
+
+/-
+  definition htpy_of_ab_qg_group {K L : property A} [is_subgroup A K] [is_subgroup A L] (K_in_L : Π (a : A), K a → L a) (L_in_K : Π (a : A), L a → K a) :  iso_of_ab_qg_group K_in_L L_in_K ∘g ab_qg_map K ~ ab_qg_map L :=
+  begin
+    fapply htpy_of_ab_qg_group'
+  end
+-/
+  end quotient_group_iso_ua
+
+  section quotient_group_iso
+  variables {K L : property A} [is_subgroup A K] [is_subgroup A L] (H1 : Π (a : A), K a → L a) (H2 : Π (a : A), L a → K a)
+  include H1
+  include H2
+
+  definition quotient_group_iso_contr_KL_map :
+    quotient_ab_group K →g quotient_ab_group L :=
+    pr1 (center' (quotient_group_functor_contr H1))
+
+  definition quotient_group_iso_contr_KL_triangle :
+    quotient_group_iso_contr_KL_map H1 H2 ∘g ab_qg_map K ~ ab_qg_map L :=
+    pr2 (center' (quotient_group_functor_contr H1))
+
+  definition quotient_group_iso_contr_KK :
+    is_contr (Σ (g : quotient_ab_group K →g quotient_ab_group K), g ∘g ab_qg_map K ~ ab_qg_map K) :=
+    @quotient_group_functor_contr A K K _ _ (λ a, H2 a ∘ H1 a)
+
+  definition quotient_group_iso_contr_LK :
+    quotient_ab_group L →g quotient_ab_group K :=
+    pr1 (center' (@quotient_group_functor_contr A L K _ _ H2))
+
+  definition quotient_group_iso_contr_LL :
+    quotient_ab_group L →g quotient_ab_group L :=
+    pr1 (center' (@quotient_group_functor_contr A L L _ _ (λ a, H1 a ∘ H2 a)))
+
+/-
+  definition quotient_group_iso : quotient_ab_group K ≃g quotient_ab_group L :=
+    begin
+      fapply isomorphism.mk,
+      exact pr1 (center' (quotient_group_iso_contr_KL H1 H2)),
+      fapply adjointify,
+      exact quotient_group_iso_contr_LK H1 H2,
+      intro x,
+      induction x, reflexivity,
+    end
+-/
+
+  definition quotient_group_iso_contr_aux  :
+    is_contr (Σ(gh : Σ (g : quotient_ab_group K →g quotient_ab_group L), g ∘g ab_qg_map K ~ ab_qg_map L), is_equiv (group_fun (pr1 gh))) :=
+  begin
+    fapply is_trunc_sigma,
+    exact quotient_group_functor_contr H1,
+    intro a, induction a with g h,
+    fapply is_contr_of_inhabited_prop,
+    fapply adjointify,
+    rexact group_fun (pr1 (center' (@quotient_group_functor_contr A L K _ _ H2))),
+    note htpy := homotopy_of_eq (ap group_fun (ap sigma.pr1 (@quotient_group_functor_id _ L _ (λ a, (H1 a) ∘ (H2 a))))),
+    have KK : is_contr ((Σ(g' : quotient_ab_group K →g quotient_ab_group K), g' ∘g ab_qg_map K ~ ab_qg_map K) ), from
+      quotient_group_functor_contr (λ a, (H2 a) ∘ (H1 a)),
+    -- have KK_path : ⟨g, h⟩ = ⟨id, λ a, refl (ab_qg_map K a)⟩, from eq_of_is_contr ⟨g, h⟩ ⟨id, λ a, refl (ab_qg_map K a)⟩,
+    repeat exact sorry
+  end
+/-
+  definition quotient_group_iso_contr {K L : property A} [is_subgroup A K] [is_subgroup A L] (H1 : Π (a : A), K a → L a) (H2 : Π (a : A), L a → K a) :
+    is_contr (Σ (g : quotient_ab_group K ≃g quotient_ab_group L), g ∘g ab_qg_map K ~ ab_qg_map L) :=
+  begin
+    refine @is_trunc_equiv_closed (Σ(gh : Σ (g : quotient_ab_group K →g quotient_ab_group L), g ∘g ab_qg_map K ~ ab_qg_map L), is_equiv (group_fun (pr1 gh))) (Σ (g : quotient_ab_group K ≃g quotient_ab_group L), g ∘g ab_qg_map K ~ ab_qg_map L) -2 _ (quotient_group_iso_contr_aux H1 H2),
+  exact calc
+    (Σ gh, is_equiv (group_fun gh.1)) ≃ Σ (g : quotient_ab_group K →g quotient_ab_group L) (h : g ∘g ab_qg_map K ~ ab_qg_map L), is_equiv (group_fun g) : by exact (sigma_assoc_equiv (λ gh, is_equiv (group_fun gh.1)))⁻¹
+    ... ≃ (Σ (g : quotient_ab_group K ≃g quotient_ab_group L), g ∘g ab_qg_map K ~ ab_qg_map L) : _
+  end
+-/
+
+  end quotient_group_iso
+
+  definition quotient_group_functor [constructor] (φ : G →g G') (h : Πg, g ∈ N → φ g ∈ N') :
+    quotient_group N →g quotient_group N' :=
+  begin
+    apply quotient_group_elim (qg_map N' ∘g φ),
+    intro g Ng, esimp,
+    refine qg_map_eq_one (φ g) (h g Ng)
+  end
+
+------------------------------------------------
+  -- FIRST ISOMORPHISM THEOREM
+------------------------------------------------
+
+definition kernel_quotient_extension {A B : AbGroup} (f : A →g B) : quotient_ab_group (kernel f) →g B :=
+  begin
+    unfold quotient_ab_group,
+    fapply @quotient_group_elim A B _ (@is_normal_subgroup_ab _ (kernel f) _) f,
+    intro a, intro p, exact p
+  end
+
+definition kernel_quotient_extension_triangle {A B : AbGroup} (f : A →g B) :
+  kernel_quotient_extension f ∘ ab_qg_map (kernel f) ~ f :=
+  begin
+    intro a,
+    apply @quotient_group_compute _ _ _ (@is_normal_subgroup_ab _ (kernel f) _)
+  end
+
+definition is_embedding_kernel_quotient_extension {A B : AbGroup} (f : A →g B) :
+  is_embedding (kernel_quotient_extension f) :=
+  begin
+    fapply is_embedding_of_is_mul_hom,
+    intro x,
+    note H := is_surjective_ab_qg_map (kernel f) x,
+    induction H, induction p,
+    intro q,
+    apply @qg_map_eq_one _ _ (@is_normal_subgroup_ab _ (kernel f) _),
+    refine _ ⬝ q,
+    symmetry,
+    rexact kernel_quotient_extension_triangle f a
+  end
+
+definition ab_group_quotient_homomorphism (A B : AbGroup)(K : property A)(L : property B) [is_subgroup A K] [is_subgroup B L] (f : A →g B)
+     (p : Π(a:A), a ∈ K → f a ∈ L) : quotient_ab_group K →g quotient_ab_group L :=
+    begin
+    fapply @quotient_group_elim,
+    exact (ab_qg_map L) ∘g f,
+    intro a,
+    intro k,
+    exact @ab_qg_map_eq_one B L _ (f a) (p a k),
+    end
+
+definition ab_group_kernel_factor {A B C: AbGroup} (f : A →g B)(g : A →g C){i : C →g B}(H : f = i ∘g g )
+           : kernel g ⊆ kernel f :=
+  begin
+   intro a,
+   intro p,
+   exact calc
+     f a = i (g a)            : homotopy_of_eq (ap group_fun H) a
+     ... = i 1                : ap i p
+     ... = 1                  : respect_one i
+  end
+
+definition  ab_group_triv_kernel_factor {A B C: AbGroup} (f : A →g B)(g : A →g C){i : C →g B}(H : f = i ∘g g ) :
+ kernel f ⊆ '{1} → kernel g ⊆ '{1} :=
+λ p, subproperty.trans (ab_group_kernel_factor f g H) p
+
+definition is_embedding_of_kernel_subproperty_one {A B : AbGroup} (f : A →g B) :
+  kernel f ⊆ '{1} → is_embedding f :=
+λ p, is_embedding_of_is_mul_hom _
+  (take x, assume h : f x = 1,
+    show x = 1, from eq_of_mem_singleton (p _ h))
+
+definition kernel_subproperty_one {A B : AbGroup} (f : A →g B) :
+  is_embedding f → kernel f ⊆ '{1} :=
+λ h x hx,
+  have x = 1, from eq_one_of_is_mul_hom hx,
+  show x ∈ '{1}, from mem_singleton_of_eq this
+
+definition ab_group_kernel_equivalent {A B : AbGroup} (C : AbGroup) (f : A →g B)(g : A →g C)(i : C →g B)(H : f = i ∘g g )(K : is_embedding i)
+           : Π a:A, a ∈ kernel g ↔ a ∈ kernel f :=
+exteq_of_subproperty_of_subproperty
+  (show kernel g ⊆ kernel f, from ab_group_kernel_factor f g H)
+  (show kernel f ⊆ kernel g, from
+    take a,
+    suppose f a = 1,
+    have i (g a) = i 1, from calc
+      i (g a) = f a       : (homotopy_of_eq (ap group_fun H) a)⁻¹
+          ... = 1         : this
+          ... = i 1       : (respect_one i)⁻¹,
+    is_injective_of_is_embedding this)
+
+definition ab_group_kernel_image_lift (A B : AbGroup) (f : A →g B)
+           : Π a : A, a ∈ kernel (image_lift f) ↔ a ∈ kernel f :=
+  begin
+    fapply ab_group_kernel_equivalent (ab_Image f) (f) (image_lift(f)) (image_incl(f)),
+    exact image_factor f,
+    exact is_embedding_of_is_injective (image_incl_injective(f)),
+  end
+
+definition ab_group_kernel_quotient_to_image {A B : AbGroup} (f : A →g B)
+           : quotient_ab_group (kernel f) →g ab_Image (f) :=
+  begin
+           fapply quotient_ab_group_elim (image_lift f), intro a, intro p,
+           apply iff.mpr (ab_group_kernel_image_lift _ _ f a) p
+  end
+
+definition ab_group_kernel_quotient_to_image_domain_triangle {A B : AbGroup} (f : A →g B)
+           :  ab_group_kernel_quotient_to_image (f) ∘g ab_qg_map (kernel f) ~ image_lift(f) :=
+  begin
+    intros a,
+    esimp,
+  end
+
+definition ab_group_kernel_quotient_to_image_codomain_triangle {A B : AbGroup} (f : A →g B)
+           : image_incl f ∘g ab_group_kernel_quotient_to_image f ~ kernel_quotient_extension f :=
+  begin
+    intro x,
+    induction x,
+    reflexivity,
+    fapply is_prop.elimo
+  end
+
+definition is_surjective_kernel_quotient_to_image {A B : AbGroup} (f : A →g B)
+           : is_surjective (ab_group_kernel_quotient_to_image f) :=
+  begin
+    fapply is_surjective_factor (group_fun (ab_qg_map (kernel f))),
+    exact image_lift f,
+    apply @quotient_group_compute _ _ _ (@is_normal_subgroup_ab _ (kernel f) _),
+    exact is_surjective_image_lift f
+  end
+
+definition is_embedding_kernel_quotient_to_image {A B : AbGroup} (f : A →g B)
+           : is_embedding (ab_group_kernel_quotient_to_image f) :=
+  begin
+    fapply is_embedding_factor (ab_group_kernel_quotient_to_image f) (image_incl f) (kernel_quotient_extension f),
+    exact ab_group_kernel_quotient_to_image_codomain_triangle f,
+    exact is_embedding_kernel_quotient_extension f
+  end
+
+definition ab_group_first_iso_thm {A B : AbGroup} (f : A →g B)
+           : quotient_ab_group (kernel f) ≃g ab_Image f :=
+  begin
+    fapply isomorphism.mk,
+    exact ab_group_kernel_quotient_to_image f,
+    fapply is_equiv_of_is_surjective_of_is_embedding,
+    exact is_embedding_kernel_quotient_to_image f,
+    exact is_surjective_kernel_quotient_to_image f
+  end
+
+definition codomain_surjection_is_quotient {A B : AbGroup} (f : A →g B)( H : is_surjective f)
+           : quotient_ab_group (kernel f) ≃g B :=
+    begin
+     exact (ab_group_first_iso_thm f) ⬝g (iso_surjection_ab_image_incl f H)
+   end
+
+definition codomain_surjection_is_quotient_triangle {A B : AbGroup} (f : A →g B)( H : is_surjective f)
+           : codomain_surjection_is_quotient (f)(H) ∘g ab_qg_map (kernel f) ~ f :=
+     begin
+    intro a,
+    esimp
+     end
+
+-- print iff.mpr
+    /- set generating normal subgroup -/
+
+  section
+
+    parameters {A₁ : AbGroup} (S : A₁ → Prop)
+    variable {A₂ : AbGroup}
+
+    inductive generating_relation' : A₁ → Type :=
+    | rincl : Π{g}, S g → generating_relation' g
+    | rmul  : Π{g h}, generating_relation' g → generating_relation' h → generating_relation' (g * h)
+    | rinv  : Π{g}, generating_relation' g → generating_relation' g⁻¹
+    | rone  : generating_relation' 1
+    open generating_relation'
+    definition generating_relation (g : A₁) : Prop := ∥ generating_relation' g ∥
+    local abbreviation R := generating_relation
+    definition gr_one : R 1 := tr (rone S)
+    definition gr_inv (g : A₁) : R g → R g⁻¹ :=
+    trunc_functor -1 rinv
+    definition gr_mul (g h : A₁) : R g → R h → R (g * h) :=
+    trunc_functor2 rmul
+
+    definition normal_generating_relation [instance] : is_subgroup A₁ generating_relation :=
+    ⦃ is_subgroup,
+      one_mem := gr_one,
+      inv_mem := gr_inv,
+      mul_mem := gr_mul⦄
+
+    parameter (A₁)
+    definition quotient_ab_group_gen : AbGroup := quotient_ab_group generating_relation
+
+    definition gqg_map [constructor] : A₁ →g quotient_ab_group_gen :=
+    ab_qg_map _
+
+    parameter {A₁}
+    definition gqg_eq_of_rel {g h : A₁} (H : S (g * h⁻¹)) : gqg_map g = gqg_map h :=
+    eq_of_rel (tr (rincl H))
+
+    -- this one might work if the previous one doesn't (maybe make this the default one?)
+    definition gqg_eq_of_rel' {g h : A₁} (H : S (g * h⁻¹)) : class_of g = class_of h :> quotient_ab_group_gen :=
+    gqg_eq_of_rel H
+
+    definition gqg_elim [constructor] (f : A₁ →g A₂) (H : Π⦃g⦄, S g → f g = 1)
+      : quotient_ab_group_gen →g A₂ :=
+    begin
+      apply quotient_ab_group_elim f,
+      intro g r, induction r with r,
+      induction r with g s g h r r' IH1 IH2 g r IH,
+      { exact H s },
+      { exact !respect_mul ⬝ ap011 mul IH1 IH2 ⬝ !one_mul },
+      { exact !respect_inv ⬝ ap inv IH ⬝ !one_inv },
+      { apply respect_one }
+    end
+
+    definition gqg_elim_compute (f : A₁ →g A₂) (H : Π⦃g⦄, S g → f g = 1)
+      : gqg_elim f H ∘ gqg_map ~ f :=
+    begin
+      intro g, reflexivity
+    end
+
+    definition gqg_elim_unique (f : A₁ →g A₂) (H : Π⦃g⦄, S g → f g = 1)
+      (k : quotient_ab_group_gen →g A₂) : ( k ∘g gqg_map ~ f ) → k ~ gqg_elim f H :=
+    !ab_gelim_unique
+
+  end
+
+end group
+
+namespace group
+
+  variables {G H K : Group} {R : property G} [is_normal_subgroup G R]
+                            {S : property H} [is_normal_subgroup H S]
+                            {T : property K} [is_normal_subgroup K T]
+
+  theorem quotient_group_functor_compose (ψ : H →g K) (φ : G →g H)
+    (hψ : Πg, g ∈ S → ψ g ∈ T) (hφ : Πg, g ∈ R → φ g ∈ S) :
+    quotient_group_functor ψ hψ ∘g quotient_group_functor φ hφ ~
+    quotient_group_functor (ψ ∘g φ) (λg, proof hψ (φ g) qed ∘ hφ g) :=
+  begin
+    intro g, induction g using set_quotient.rec_prop with g hg, reflexivity
+  end
+
+  definition quotient_group_functor_gid :
+    quotient_group_functor (gid G) (λg, id) ~ gid (quotient_group R) :=
+  begin
+    intro g, induction g using set_quotient.rec_prop with g hg, reflexivity
+  end
+
+  definition quotient_group_functor_homotopy {ψ φ : G →g H} (hψ : Πg, R g → S (ψ g))
+    (hφ : Πg, g ∈ R → φ g ∈ S) (p : φ ~ ψ) :
+    quotient_group_functor φ hφ ~ quotient_group_functor ψ hψ :=
+  begin
+    intro g, induction g using set_quotient.rec_prop with g hg,
+    exact ap set_quotient.class_of (p g)
+  end
+
+end group
+
+namespace group
+
+  variables {G H K : AbGroup} {R : property G} [is_subgroup G R]
+                            {S : property H} [is_subgroup H S]
+                            {T : property K} [is_subgroup K T]
+
+
+  definition quotient_ab_group_functor [constructor] (φ : G →g H)
+    (h : Πg, g ∈ R → φ g ∈ S) : quotient_ab_group R →g quotient_ab_group S :=
+  @quotient_group_functor G H R (is_normal_subgroup_ab _) S (is_normal_subgroup_ab _) φ h
+
+  definition quotient_ab_group_functor_mul
+    (ψ φ : G →g H) (hψ : Πg, g ∈ R → ψ g ∈ S) (hφ : Πg, g ∈ R → φ g ∈ S) :
+    homomorphism_mul (quotient_ab_group_functor ψ hψ) (quotient_ab_group_functor φ hφ) ~
+    quotient_ab_group_functor (homomorphism_mul ψ φ)
+                        (λg hg, is_subgroup.mul_mem (hψ g hg) (hφ g hg)) :=
+  begin
+    intro g, induction g using set_quotient.rec_prop with g hg, reflexivity
+  end
+
+  theorem quotient_ab_group_functor_compose (ψ : H →g K) (φ : G →g H)
+    (hψ : Πg, g ∈ S → ψ g ∈ T) (hφ : Πg, g ∈ R → φ g ∈ S) :
+    quotient_ab_group_functor ψ hψ ∘g quotient_ab_group_functor φ hφ ~
+    quotient_ab_group_functor (ψ ∘g φ) (λg, proof hψ (φ g) qed ∘ hφ g) :=
+  @quotient_group_functor_compose G H K R _ S _ T _ ψ φ  hψ hφ 
+
+  definition quotient_ab_group_functor_gid :
+    quotient_ab_group_functor (gid G) (λg, id) ~ gid (quotient_ab_group R) :=
+  @quotient_group_functor_gid G R _
+
+  definition quotient_ab_group_functor_homotopy {ψ φ : G →g H} (hψ : Πg, R g → S (ψ g))
+    (hφ : Πg, g ∈ R → φ g ∈ S) (p : φ ~ ψ) :
+    quotient_ab_group_functor φ hφ ~ quotient_ab_group_functor ψ hψ :=
+  @quotient_group_functor_homotopy G H R _ S _ ψ φ hψ hφ p
+
+end group