diff --git a/algebra/exact_couple.hlean b/algebra/exact_couple.hlean
index 20e0b1d..2d8a1ff 100644
--- a/algebra/exact_couple.hlean
+++ b/algebra/exact_couple.hlean
@@ -6,13 +6,14 @@ Authors: Egbert Rijke, Steve Awodey
 Exact couple, derived couples, and so on
 -/
 
+/-
 import algebra.group_theory hit.set_quotient types.sigma types.list types.sum .quotient_group .subgroup .ses
 
 open eq algebra is_trunc set_quotient relation sigma sigma.ops prod prod.ops sum list trunc function group trunc
      equiv is_equiv
 
 -- This definition needs to be moved to exactness.hlean. However we had trouble doing so. Please help.
-definition iso_ker_im_of_exact {A B C : AbGroup} (f : A →g B) (g : B →g C) (E : is_exact f g) : ab_kernel g ≃g ab_image f :=
+definition iso_ker_im_of_exact {A B C : AbGroup} (f : A →g B) (g : B →g C) (E : is_exact f g) : ab_Kernel g ≃g ab_image f :=
   begin
   fapply ab_subgroup_iso,
   intro a,
@@ -283,3 +284,5 @@ definition derived_couple_exact_ij : is_exact_ag derived_couple_i derived_couple
   end
 
 end derived_couple
+
+-/
diff --git a/algebra/exactness.hlean b/algebra/exactness.hlean
index 95129cd..1af74b2 100644
--- a/algebra/exactness.hlean
+++ b/algebra/exactness.hlean
@@ -6,7 +6,7 @@ Authors: Jeremy Avigad
 Short exact sequences
 -/
 import homotopy.chain_complex eq2 .quotient_group
-open pointed is_trunc equiv is_equiv eq algebra group trunc function fiber sigma
+open pointed is_trunc equiv is_equiv eq algebra group trunc function fiber sigma property
 
 structure is_exact_t {A B : Type} {C : Type*} (f : A → B) (g : B → C) :=
   ( im_in_ker : Π(a:A), g (f a) = pt)
@@ -146,7 +146,7 @@ begin
 end
 
 definition is_exact_incl_of_subgroup {G H : Group} (f : G →g H) :
-  is_exact (incl_of_subgroup (kernel_subgroup f)) f :=
+  is_exact (incl_of_subgroup (kernel f)) f :=
 begin
   apply is_exact.mk,
   { intro x, cases x with x p, exact p },
@@ -155,7 +155,7 @@ end
 
 definition isomorphism_kernel_of_is_exact {G₄ G₃ G₂ G₁ : Group}
   {h : G₄ →g G₃} {g : G₃ →g G₂} {f : G₂ →g G₁} (H1 : is_exact h g) (H2 : is_exact g f)
-  (HG : is_contr G₄) : G₃ ≃g kernel f :=
+  (HG : is_contr G₄) : G₃ ≃g Kernel f :=
 isomorphism_left_of_is_exact_g H2 (is_exact_incl_of_subgroup f)
   (is_embedding_of_is_exact_g H1) (is_embedding_incl_of_subgroup _)
 
@@ -221,7 +221,7 @@ end
 
 /- TODO: move and remove other versions -/
 
-  definition is_surjective_qg_map {A : Group} (N : normal_subgroup_rel A) :
+  definition is_surjective_qg_map {A : Group} (N : property A) [is_normal_subgroup A N] :
     is_surjective (qg_map N) :=
   begin
     intro x, induction x,
@@ -230,11 +230,12 @@ end
     apply is_prop.elimo
   end
 
-  definition is_surjective_ab_qg_map {A : AbGroup} (N : subgroup_rel A) :
+  definition is_surjective_ab_qg_map {A : AbGroup} (N : property A) [is_normal_subgroup A N] :
     is_surjective (ab_qg_map N) :=
-  is_surjective_qg_map _
+  is_surjective_ab_qg_map _
 
-  definition qg_map_eq_one {A : Group} {K : normal_subgroup_rel A} (g : A) (H : K g) :
+  definition qg_map_eq_one {A : Group} {K : property A} [is_normal_subgroup A K] (g : A)
+      (H : g ∈ K) :
     qg_map K g = 1 :=
   begin
     apply set_quotient.eq_of_rel,
@@ -245,11 +246,12 @@ end
     exact transport (λx, K x) e⁻¹ H
   end
 
-  definition ab_qg_map_eq_one {A : AbGroup} {K : subgroup_rel A} (g : A) (H : K g) :
+  definition ab_qg_map_eq_one {A : AbGroup} {K : property A} [is_subgroup A K] (g : A)
+      (H : g ∈ K) :
     ab_qg_map K g = 1 :=
-  qg_map_eq_one g H
+  ab_qg_map_eq_one g H
 
-definition is_short_exact_normal_subgroup {G : Group} (S : normal_subgroup_rel G) :
+definition is_short_exact_normal_subgroup {G : Group} (S : property G) [is_normal_subgroup G S] :
   is_short_exact (incl_of_subgroup S) (qg_map S) :=
 begin
   fconstructor,
diff --git a/algebra/graded.hlean b/algebra/graded.hlean
index 42f9361..c7a9194 100644
--- a/algebra/graded.hlean
+++ b/algebra/graded.hlean
@@ -5,7 +5,7 @@
 import .left_module .direct_sum .submodule --..heq
 
 open is_trunc algebra eq left_module pointed function equiv is_equiv prod group sigma sigma.ops nat
-  trunc_index
+  trunc_index property
 namespace left_module
 
 definition graded [reducible] (str : Type) (I : Type) : Type := I → str
@@ -421,20 +421,24 @@ LeftModule_of_AddAbGroup (dirsum' N) (λr n, dirsum_smul r n)
 
 /- graded variants of left-module constructions -/
 
-definition graded_submodule [constructor] (S : Πi, submodule_rel (M i)) : graded_module R I :=
+definition graded_submodule [constructor] (S : Πi, property (M i)) [Π i, is_submodule (M i) (S i)] :
+  graded_module R I :=
 λi, submodule (S i)
 
-definition graded_submodule_incl [constructor] (S : Πi, submodule_rel (M i)) :
+definition graded_submodule_incl [constructor] (S : Πi, property (M i)) [H : Π i, is_submodule (M i) (S i)] :
   graded_submodule S →gm M :=
+have Π i, is_submodule (M (to_fun erfl i)) (S i), from H,
 graded_hom.mk erfl (λi, submodule_incl (S i))
 
-definition graded_hom_lift [constructor] {S : Πi, submodule_rel (M₂ i)}
+definition graded_hom_lift [constructor] (S : Πi, property (M₂ i)) [Π i, is_submodule (M₂ i) (S i)]
   (φ : M₁ →gm M₂)
-  (h : Π(i : I) (m : M₁ i), S (deg φ i) (φ i m)) : M₁ →gm graded_submodule S :=
+  (h : Π(i : I) (m : M₁ i), φ i m ∈ S (deg φ i)) : M₁ →gm graded_submodule S :=
 graded_hom.mk (deg φ) (λi, hom_lift (φ i) (h i))
 
-definition graded_submodule_functor [constructor] {S : Πi, submodule_rel (M₁ i)}
-  {T : Πi, submodule_rel (M₂ i)} (φ : M₁ →gm M₂)
+definition graded_submodule_functor [constructor]
+  {S : Πi, property (M₁ i)} [Π i, is_submodule (M₁ i) (S i)]
+  {T : Πi, property (M₂ i)} [Π i, is_submodule (M₂ i) (T i)]
+  (φ : M₁ →gm M₂)
   (h : Π(i : I) (m : M₁ i), S i m → T (deg φ i) (φ i m)) :
   graded_submodule S →gm graded_submodule T :=
 graded_hom.mk (deg φ) (λi, submodule_functor (φ i) (h i))
@@ -588,24 +592,25 @@ end
 definition graded_kernel (f : M₁ →gm M₂) : graded_module R I :=
 λi, kernel_module (f i)
 
-definition graded_quotient (S : Πi, submodule_rel (M i)) : graded_module R I :=
+definition graded_quotient (S : Πi, property (M i)) [Π i, is_submodule (M i) (S i)] : graded_module R I :=
 λi, quotient_module (S i)
 
-definition graded_quotient_map [constructor] (S : Πi, submodule_rel (M i)) :
+definition graded_quotient_map [constructor] (S : Πi, property (M i)) [Π i, is_submodule (M i) (S i)] :
   M →gm graded_quotient S :=
 graded_hom.mk erfl (λi, quotient_map (S i))
 
-definition graded_quotient_elim [constructor] {S : Πi, submodule_rel (M i)} (φ : M →gm M₂)
+definition graded_quotient_elim [constructor]
+  (S : Πi, property (M i)) [Π i, is_submodule (M i) (S i)]
+  (φ : M →gm M₂)
   (H : Πi ⦃m⦄, S i m → φ i m = 0) : graded_quotient S →gm M₂ :=
 graded_hom.mk (deg φ) (λi, quotient_elim (φ i) (H i))
 
 definition graded_homology (g : M₂ →gm M₃) (f : M₁ →gm M₂) : graded_module R I :=
-graded_quotient (λi, submodule_rel_submodule (kernel_rel (g i)) (image_rel (f ← i)))
+graded_quotient (λ i, homology_quotient_property (g i) (f ← i))
 
 -- the two reasonable definitions of graded_homology are definitionally equal
 example (g : M₂ →gm M₃) (f : M₁ →gm M₂) :
-  (λi, homology (g i) (f ← i)) =
-  graded_quotient (λi, submodule_rel_submodule (kernel_rel (g i)) (image_rel (f ← i))) := idp
+  (λi, homology (g i) (f ← i)) = graded_homology g f := idp
 
 definition graded_homology.mk (g : M₂ →gm M₃) (f : M₁ →gm M₂) {i : I} (m : M₂ i) (h : g i m = 0) :
   graded_homology g f i :=
@@ -613,18 +618,18 @@ homology.mk _ m h
 
 definition graded_homology_intro [constructor] (g : M₂ →gm M₃) (f : M₁ →gm M₂) :
   graded_kernel g →gm graded_homology g f :=
-graded_quotient_map _
+@graded_quotient_map _ _ _ (λ i, homology_quotient_property (g i) (f ← i)) _
 
 definition graded_homology_elim {g : M₂ →gm M₃} {f : M₁ →gm M₂} (h : M₂ →gm M)
   (H : compose_constant h f) : graded_homology g f →gm M :=
 graded_hom.mk (deg h) (λi, homology_elim (h i) (H _ _))
 
-open trunc
 definition image_of_graded_homology_intro_eq_zero {g : M₂ →gm M₃} {f : M₁ →gm M₂}
   ⦃i j : I⦄ (p : deg f i = j) (m : graded_kernel g j) (H : graded_homology_intro g f j m = 0) :
   image (f ↘ p) m.1 :=
 begin
-  induction p, exact graded_hom_change_image _ _ (rel_of_quotient_map_eq_zero m H)
+  induction p, exact graded_hom_change_image _ _
+    (@rel_of_quotient_map_eq_zero _ _ _ _ m H)
 end
 
 definition is_exact_gmod (f : M₁ →gm M₂) (f' : M₂ →gm M₃) : Type :=
diff --git a/algebra/product_group.hlean b/algebra/product_group.hlean
index 066e18a..fd8c2fe 100644
--- a/algebra/product_group.hlean
+++ b/algebra/product_group.hlean
@@ -12,7 +12,7 @@ open eq algebra is_trunc set_quotient relation sigma prod prod.ops sum list trun
      equiv
 namespace group
 
-  variables {G G' : Group} (H : subgroup_rel G) (N : normal_subgroup_rel G) {g g' h h' k : G}
+  variables {G G' : Group} {g g' h h' k : G}
             {A B : AbGroup}
 
   /- Binary products (direct product) of Groups -/
diff --git a/algebra/quotient_group.hlean b/algebra/quotient_group.hlean
deleted file mode 100644
index 8958b9e..0000000
--- a/algebra/quotient_group.hlean
+++ /dev/null
@@ -1,716 +0,0 @@
-/-
-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]
-
-  definition quotient_ab_group_functor [constructor] {G H : AbGroup}
-     {R : property G} [is_subgroup G R]
-     {S : property H} [is_subgroup H S] (φ : 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
-
-  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_mul
-    {G H : AbGroup} {R : property G} [is_subgroup G R] {S : property H} [is_subgroup H S]
-    (ψ φ : 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
-
-  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
diff --git a/algebra/ses.hlean b/algebra/ses.hlean
index e03603d..89f0eea 100644
--- a/algebra/ses.hlean
+++ b/algebra/ses.hlean
@@ -11,7 +11,7 @@ At the moment, it only covers short exact sequences of abelian groups, but this
 import algebra.group_theory hit.set_quotient types.sigma types.list types.sum .quotient_group .subgroup .exactness
 
 open eq algebra is_trunc set_quotient relation sigma sigma.ops prod prod.ops sum list trunc function group trunc
-     equiv is_equiv
+     equiv is_equiv property
 
 structure SES (A B C : AbGroup) :=
   ( f : A →g B)
@@ -20,23 +20,23 @@ structure SES (A B C : AbGroup) :=
   ( Hg : is_surjective g)
   ( ex : is_exact_ag f g)
 
-definition SES_of_inclusion {A B : AbGroup} (f : A →g B) (Hf : is_embedding f) : SES A B (quotient_ab_group (image_subgroup f)) :=
+definition SES_of_inclusion {A B : AbGroup} (f : A →g B) (Hf : is_embedding f) : SES A B (quotient_ab_group (image f)) :=
   begin
-    have Hg : is_surjective (ab_qg_map (image_subgroup f)),
-    from is_surjective_ab_qg_map (image_subgroup f),
+    have Hg : is_surjective (ab_qg_map (image f)),
+    from is_surjective_ab_qg_map (image f),
     fapply SES.mk,
     exact f,
-    exact ab_qg_map (image_subgroup f),
+    exact ab_qg_map (image f),
     exact Hf,
     exact Hg,
     fapply is_exact.mk,
     intro a,
-    fapply qg_map_eq_one, fapply tr, fapply fiber.mk, exact a, reflexivity,
+    fapply ab_qg_map_eq_one, fapply tr, fapply fiber.mk, exact a, reflexivity,
     intro b, intro p,
     exact rel_of_ab_qg_map_eq_one _ p
   end
 
-definition SES_of_subgroup {B : AbGroup} (S : subgroup_rel B) : SES (ab_subgroup S) B (quotient_ab_group S) :=
+definition SES_of_subgroup {B : AbGroup} (S : property B) [is_subgroup B S] : SES (ab_subgroup S) B (quotient_ab_group S) :=
   begin
     fapply SES.mk,
     exact incl_of_subgroup S,
@@ -48,10 +48,10 @@ definition SES_of_subgroup {B : AbGroup} (S : subgroup_rel B) : SES (ab_subgroup
     intro b p, fapply tr, fapply fiber.mk, fapply sigma.mk b, fapply rel_of_ab_qg_map_eq_one, exact p, reflexivity,
   end
 
-definition SES_of_surjective_map {B C : AbGroup} (g : B →g C) (Hg : is_surjective g) : SES (ab_kernel g) B C :=
+definition SES_of_surjective_map {B C : AbGroup} (g : B →g C) (Hg : is_surjective g) : SES (ab_Kernel g) B C :=
   begin
     fapply SES.mk,
-    exact ab_kernel_incl g,
+    exact ab_Kernel_incl g,
     exact g,
     exact is_embedding_ab_kernel_incl g,
     exact Hg,
@@ -60,10 +60,10 @@ definition SES_of_surjective_map {B C : AbGroup} (g : B →g C) (Hg : is_surject
     intro b p, fapply tr, fapply fiber.mk, fapply sigma.mk, exact b, exact p, reflexivity,
   end
 
-definition SES_of_homomorphism {A B : AbGroup} (f : A →g B) : SES (ab_kernel f) A (ab_image f) :=
+definition SES_of_homomorphism {A B : AbGroup} (f : A →g B) : SES (ab_Kernel f) A (ab_Image f) :=
   begin
     fapply SES.mk,
-    exact ab_kernel_incl f,
+    exact ab_Kernel_incl f,
     exact image_lift f,
     exact is_embedding_ab_kernel_incl f,
     exact is_surjective_image_lift f,
@@ -106,8 +106,8 @@ parameters {A B C : AbGroup} (ses : SES A B C)
   local abbreviation f := SES.f ses
   local notation `g` := SES.g ses
   local abbreviation ex := SES.ex ses
-  local abbreviation q := ab_qg_map (kernel_subgroup g)
-  local abbreviation B_mod_A := quotient_ab_group (kernel_subgroup g)
+  local abbreviation q := ab_qg_map (kernel g)
+  local abbreviation B_mod_A := quotient_ab_group (kernel g)
 
 definition SES_iso_stable {A' B' C' : AbGroup} (f' : A' →g B') (g' : B' →g C') (α : A' ≃g A) (β : B' ≃g B) (γ : C' ≃g C) (Hαβ : f ∘g α ~ β ∘g f') (Hβγ : g ∘g β ~ γ ∘g g') : SES A' B' C' :=
   begin
@@ -142,9 +142,9 @@ begin
   rewrite [(H a')⁻¹],
   fapply is_exact.im_in_ker (SES.ex ses),
   intro b p,
-  have  t : trunctype.carrier (subgroup_to_rel (image_subgroup f) b), from is_exact.ker_in_im (SES.ex ses) b p,
-  induction t, fapply tr, induction a with a q, fapply fiber.mk, exact α⁻¹ᵍ a, rewrite [(H (α⁻¹ᵍ a))⁻¹],
-  krewrite [right_inv (equiv_of_isomorphism α) a], assumption
+  have  t : image' f b, from is_exact.ker_in_im (SES.ex ses) b p,
+  unfold image' at t, induction t, fapply tr, induction a with a h, fapply fiber.mk, exact α⁻¹ᵍ a, rewrite [(H (α⁻¹ᵍ a))⁻¹],
+  krewrite [right_inv (equiv_of_isomorphism α) a], exact h
 end
 
 --definition quotient_SES {A B C : AbGroup} (ses : SES A B C) :
@@ -194,7 +194,7 @@ definition quotient_triangle_extend_SES {C': AbGroup} (k : B →g C') :
   local abbreviation f' := SES.f ses'
   local notation `g'` := SES.g ses'
   local abbreviation ex' := SES.ex ses'
-  local abbreviation q' := ab_qg_map (kernel_subgroup g')
+  local abbreviation q' := ab_qg_map (kernel g')
   local abbreviation α' := quotient_codomain_SES
 
   include htpy1
@@ -204,8 +204,8 @@ definition quotient_triangle_extend_SES {C': AbGroup} (k : B →g C') :
     fapply @(is_trunc_equiv_closed_rev _ (quotient_triangle_extend_SES (g' ∘g hB))),
     fapply ab_qg_universal_property,
     intro b, intro K,
-    have k : trunctype.carrier (image_subgroup f b), from is_exact.ker_in_im ex b K,
-    induction k, induction a with a p,
+    have k : image' f b, from is_exact.ker_in_im ex b K,
+    unfold image' at k, induction k, induction a with a p,
     induction p,
     refine (ap g' (htpy1 a)) ⬝ _,
     fapply is_exact.im_in_ker ex' (hA a)
diff --git a/algebra/spectral_sequence.hlean b/algebra/spectral_sequence.hlean
index 58f0fe1..42eeb34 100644
--- a/algebra/spectral_sequence.hlean
+++ b/algebra/spectral_sequence.hlean
@@ -46,8 +46,7 @@ namespace left_module
   !is_contr_image_module
 
   definition i' : D' →gm D' :=
-  graded_image_lift i ∘gm graded_submodule_incl (λx, image_rel (i ← x))
-  -- degree i + 0
+  graded_image_lift i ∘gm  graded_submodule_incl (λx, image (i ← x))
 
   lemma is_surjective_i' {x y : I} (p : deg i' x = y)
     (H : Π⦃z⦄ (q : deg i z = x), is_surjective (i ↘ q)) : is_surjective (i' ↘ p) :=
@@ -69,7 +68,7 @@ namespace left_module
   end
 
   lemma j_lemma2 : Π⦃x : I⦄ ⦃m : D x⦄ (p : i x m = 0),
-    (graded_quotient_map _ ∘gm graded_hom_lift j j_lemma1) x m = 0 :> E' _ :=
+    (graded_homology_intro _ _ ∘gm graded_hom_lift _ j j_lemma1) x m = 0 :> E' _ :=
   begin
     have Π⦃x y : I⦄ (q : deg k x = y) (r : deg d x = deg j y)
       (s : ap (deg j) q = r) ⦃m : D y⦄ (p : i y m = 0), image (d ↘ r) (j y m),
@@ -90,11 +89,11 @@ namespace left_module
     end,
     intros,
     rewrite [graded_hom_compose_fn],
-    exact quotient_map_eq_zero _ (this p)
+    exact @quotient_map_eq_zero _ _ _ _ _ (this p)
   end
 
   definition j' : D' →gm E' :=
-  graded_image_elim (graded_homology_intro d d ∘gm graded_hom_lift j j_lemma1) j_lemma2
+  graded_image_elim (graded_homology_intro d d ∘gm graded_hom_lift _ j j_lemma1) j_lemma2
   -- degree deg j - deg i
 
   lemma k_lemma1 ⦃x : I⦄ (m : E x) (p : d x m = 0) : image (i ← (deg k x)) (k x m) :=
@@ -102,7 +101,7 @@ namespace left_module
 
   definition k₂ : graded_kernel d →gm D' := graded_submodule_functor k k_lemma1
 
-  lemma k_lemma2 ⦃x : I⦄ (m : E x) (h₁ : kernel_rel (d x) m) (h₂ : image (d ← x) m) :
+  lemma k_lemma2 ⦃x : I⦄ (m : E x) (h₁ : lm_kernel (d x) m) (h₂ : image (d ← x) m) :
     k₂ x ⟨m, h₁⟩ = 0 :=
   begin
     assert H₁ : Π⦃x' y z w : I⦄ (p : deg k x' = y) (q : deg j y = z) (r : deg k z = w) (n : E x'),
@@ -115,8 +114,8 @@ namespace left_module
   end
 
   definition k' : E' →gm D' :=
-  graded_quotient_elim (graded_submodule_functor k k_lemma1)
-                       (by intro x m h; exact k_lemma2 m.1 m.2 h)
+  @graded_quotient_elim _ _ _ _ _ _ (graded_submodule_functor k k_lemma1)
+                       (by intro x m h; cases m with [m1, m2]; exact k_lemma2 m1 m2 h)
 
   definition i'_eq ⦃x : I⦄ (m : D x) (h : image (i ← x) m) : (i' x ⟨m, h⟩).1 = i x m :=
   by reflexivity
@@ -125,7 +124,7 @@ namespace left_module
   by reflexivity
 
   lemma j'_eq {x : I} (m : D x) : j' ↘ (ap (deg j) (left_inv (deg i) x)) (graded_image_lift i x m) =
-    class_of (graded_hom_lift j proof j_lemma1 qed x m) :=
+    class_of (graded_hom_lift _ j proof j_lemma1 qed x m) :=
   begin
     refine graded_image_elim_destruct _ _ _ idp _ m,
     apply is_set.elim,
@@ -155,9 +154,9 @@ namespace left_module
     { revert x, refine equiv_rect (deg k) _ _, intro x,
       refine graded_image.rec _, intro m p,
       assert q : graded_homology_intro d d (deg j (deg k x))
-                   (graded_hom_lift j j_lemma1 (deg k x) m) = 0,
+                   (graded_hom_lift _ j j_lemma1 (deg k x) m) = 0,
       { exact !j'_eq⁻¹ ⬝ p },
-      note q2 := image_of_graded_homology_intro_eq_zero idp (graded_hom_lift j _ _ m) q,
+      note q2 := image_of_graded_homology_intro_eq_zero idp (graded_hom_lift _ j _ _ m) q,
       induction q2 with n r,
       assert s : j (deg k x) (m - k x n) = 0,
       { refine respect_sub (j (deg k x)) m (k x n) ⬝ _,
diff --git a/algebra/subgroup.hlean b/algebra/subgroup.hlean
index 934dad9..9af352d 100644
--- a/algebra/subgroup.hlean
+++ b/algebra/subgroup.hlean
@@ -59,7 +59,7 @@ namespace group
       that the image of f is closed under the group operations is part
       of the definition of the image of f. --/
 
-  definition image_subgroup [instance] {G : Group} {H : Group} (f : G →g H) :
+  definition is_subgroup_image [instance] {G : Group} {H : Group} (f : G →g H) :
     is_subgroup H (image f) :=
     begin
       fapply is_subgroup.mk,
@@ -177,7 +177,7 @@ section
   end
 
   -- this is just (Σ(g : G), H g), but only defined if (H g) is a prop
-  definition sg {G : Group} (H : property G) : Type := {g : G | g ∈ H}
+  definition sg {G : Group} (H : property G) : Type := subtype (λ x, x ∈ H)
   local attribute sg [reducible]
 
   definition subgroup_one [constructor] : sg H := ⟨one, subgroup_one_mem H⟩
@@ -232,9 +232,7 @@ section
 
   definition Kernel {G H : Group} (f : G →g H) : Group := subgroup (kernel f)
 
-set_option trace.class_instances true
-
-  definition ab_kernel {G H : AbGroup} (f : G →g H) : AbGroup := ab_subgroup (kernel f)
+  definition ab_Kernel {G H : AbGroup} (f : G →g H) : AbGroup := ab_subgroup (kernel f)
 
   definition incl_of_subgroup [constructor] {G : Group} (H : property G) [is_subgroup G H] :
     subgroup H →g G :=
@@ -254,12 +252,12 @@ set_option trace.class_instances true
     fapply subtype_eq
   end
 
-  definition ab_kernel_incl {G H : AbGroup} (f : G →g H) : ab_kernel f →g G :=
+  definition ab_Kernel_incl {G H : AbGroup} (f : G →g H) : ab_Kernel f →g G :=
   begin
     fapply incl_of_subgroup,
   end
 
-  definition is_embedding_ab_kernel_incl {G H : AbGroup} (f : G →g H) : is_embedding (ab_kernel_incl f) :=
+  definition is_embedding_ab_kernel_incl {G H : AbGroup} (f : G →g H) : is_embedding (ab_Kernel_incl f) :=
   begin
     fapply is_embedding_incl_of_subgroup,
   end
@@ -283,7 +281,7 @@ set_option trace.class_instances true
   definition Image {G H : Group} (f : G →g H) : Group :=
     subgroup (image f)
 
-  definition ab_image {G : AbGroup} {H : Group} (f : G →g H) : AbGroup :=
+  definition ab_Image {G : AbGroup} {H : Group} (f : G →g H) : AbGroup :=
   AbGroup_of_Group (Image f)
   begin
     intro g h,
@@ -298,11 +296,11 @@ set_option trace.class_instances true
   definition image_incl {G H : Group} (f : G →g H) : Image f →g H :=
     incl_of_subgroup (image f)
 
-definition ab_image_incl {A B : AbGroup} (f : A →g B) : ab_image f →g B := incl_of_subgroup (image f)
+definition ab_Image_incl {A B : AbGroup} (f : A →g B) : ab_Image f →g B := incl_of_subgroup (image f)
 
-definition is_equiv_surjection_ab_image_incl {A B : AbGroup} (f : A →g B) (H : is_surjective f) : is_equiv (ab_image_incl f ) :=
+definition is_equiv_surjection_ab_image_incl {A B : AbGroup} (f : A →g B) (H : is_surjective f) : is_equiv (ab_Image_incl f ) :=
   begin
-    fapply is_equiv.adjointify (ab_image_incl f),
+    fapply is_equiv.adjointify (ab_Image_incl f),
     intro b,
     fapply sigma.mk,
     exact b,
@@ -314,10 +312,10 @@ definition is_equiv_surjection_ab_image_incl {A B : AbGroup} (f : A →g B) (H :
     reflexivity
   end
 
-definition iso_surjection_ab_image_incl [constructor] {A B : AbGroup} (f : A →g B) (H : is_surjective f) : ab_image f ≃g B :=
+definition iso_surjection_ab_image_incl [constructor] {A B : AbGroup} (f : A →g B) (H : is_surjective f) : ab_Image f ≃g B :=
   begin
     fapply isomorphism.mk,
-    exact (ab_image_incl f),
+    exact (ab_Image_incl f),
     exact is_equiv_surjection_ab_image_incl f H
   end
 
@@ -355,7 +353,7 @@ f = incl_of_subgroup K ∘g hom_lift f K Hyp :=
     reflexivity
   end
 
-definition ab_hom_lift_kernel [constructor] {A B C : AbGroup} (f : A →g B) (g : B →g C) (Hyp : Π (a : A), g (f a) = 1) : A →g ab_kernel g :=
+definition ab_hom_lift_kernel [constructor] {A B C : AbGroup} (f : A →g B) (g : B →g C) (Hyp : Π (a : A), g (f a) = 1) : A →g ab_Kernel g :=
   begin
     fapply ab_hom_lift,
     exact f,
@@ -364,7 +362,7 @@ definition ab_hom_lift_kernel [constructor] {A B C : AbGroup} (f : A →g B) (g
   end
 
 definition ab_hom_lift_kernel_factors {A B C : AbGroup} (f : A →g B) (g : B →g C) (Hyp : Π (a : A), g (f a) = 1) :
-f = ab_kernel_incl g ∘g ab_hom_lift_kernel f g Hyp :=
+f = ab_Kernel_incl g ∘g ab_hom_lift_kernel f g Hyp :=
   begin
     fapply ab_hom_factors_through_lift,
   end
@@ -436,7 +434,7 @@ definition ab_image_lift [constructor] {G H : AbGroup} (f : G →g H) : G →g I
 end
 
   definition image_homomorphism {A B C : AbGroup} (f : A →g B) (g : B →g C) :
-    ab_image f →g ab_image (g ∘g f) :=
+    ab_Image f →g ab_Image (g ∘g f) :=
   begin
     fapply image_elim,
     exact image_lift (g ∘g f),
@@ -539,7 +537,7 @@ end
   end
 
   definition ab_subgroup_iso {A : AbGroup} {R S : property A} [is_subgroup A R] [is_subgroup A S]
-      (H : Π (a : A), R a -> S a) (K : Π (a : A), S a -> R a) :
+      (H : Π (a : A), a ∈ R → a ∈ S) (K : Π (a : A), a ∈ S → a ∈ R) :
     ab_subgroup R ≃g ab_subgroup S :=
   begin
     fapply isomorphism.mk,
@@ -551,7 +549,7 @@ end
   end
 
   definition ab_subgroup_iso_triangle {A : AbGroup} {R S : property A} [is_subgroup A R] [is_subgroup A S]
-      (H : Π (a : A), R a -> S a) (K : Π (a : A), S a -> R a) :
+      (H : Π (a : A), a ∈ R → a ∈ S) (K : Π (a : A), a ∈ S → a ∈ R) :
     incl_of_subgroup R  ~ incl_of_subgroup S ∘g ab_subgroup_iso H K :=
   begin
     intro r, induction r, reflexivity
@@ -560,4 +558,5 @@ end
 end group
 
 open group
-attribute image_subgroup [constructor]
+attribute is_subgroup_image [constructor]
+attribute is_subgroup_kernel [constructor]
diff --git a/algebra/submodule.hlean b/algebra/submodule.hlean
index 67e6ad3..980c375 100644
--- a/algebra/submodule.hlean
+++ b/algebra/submodule.hlean
@@ -1,40 +1,42 @@
 /- submodules and quotient modules -/
 
--- Authors: Floris van Doorn
-
-
+-- Authors: Floris van Doorn, Jeremy Avigad
 import .left_module .quotient_group
 
-open algebra eq group sigma sigma.ops is_trunc function trunc equiv is_equiv
+open algebra eq group sigma sigma.ops is_trunc function trunc equiv is_equiv property
+
+  definition group_homomorphism_of_add_group_homomorphism [constructor] {G₁ G₂ : AddGroup}
+    (φ : G₁ →a G₂) : G₁ →g G₂ :=
+  φ
 
 -- move to subgroup
-attribute normal_subgroup_rel._trans_of_to_subgroup_rel [unfold 2]
-attribute normal_subgroup_rel.to_subgroup_rel [constructor]
+-- attribute normal_subgroup_rel._trans_of_to_subgroup_rel [unfold 2]
+-- attribute normal_subgroup_rel.to_subgroup_rel [constructor]
 
-  definition is_equiv_incl_of_subgroup {G : Group} (H : subgroup_rel G) (h : Πg, H g) :
+  definition is_equiv_incl_of_subgroup {G : Group} (H : property G) [is_subgroup G H] (h : Πg, g ∈ H) :
     is_equiv (incl_of_subgroup H) :=
   have is_surjective (incl_of_subgroup H),
   begin intro g, exact image.mk ⟨g, h g⟩ idp end,
   have is_embedding (incl_of_subgroup H), from is_embedding_incl_of_subgroup H,
   function.is_equiv_of_is_surjective_of_is_embedding (incl_of_subgroup H)
 
-definition subgroup_isomorphism [constructor] {G : Group} (H : subgroup_rel G) (h : Πg, H g) :
+definition subgroup_isomorphism [constructor] {G : Group} (H : property G) [is_subgroup G H] (h : Πg, g ∈ H) :
   subgroup H ≃g G :=
 isomorphism.mk _ (is_equiv_incl_of_subgroup H h)
 
-definition is_equiv_qg_map {G : Group} (H : normal_subgroup_rel G) (H₂ : Π⦃g⦄, H g → g = 1) :
+definition is_equiv_qg_map {G : Group} (H : property G) [is_normal_subgroup G H] (H₂ : Π⦃g⦄, g ∈ H → g = 1) :
   is_equiv (qg_map H) :=
 set_quotient.is_equiv_class_of _ (λg h r, eq_of_mul_inv_eq_one (H₂ r))
 
-definition quotient_group_isomorphism [constructor] {G : Group} (H : normal_subgroup_rel G)
-  (h : Πg, H g → g = 1) : quotient_group H ≃g G :=
+definition quotient_group_isomorphism [constructor] {G : Group} (H : property G) [is_normal_subgroup G H]
+  (h : Πg, g ∈ H → g = 1) : quotient_group H ≃g G :=
 (isomorphism.mk _ (is_equiv_qg_map H h))⁻¹ᵍ
 
-definition is_equiv_ab_qg_map {G : AbGroup} (H : subgroup_rel G) (h : Π⦃g⦄, H g → g = 1) :
+definition is_equiv_ab_qg_map {G : AbGroup} (H : property G) [is_subgroup G H] (h : Π⦃g⦄, g ∈ H → g = 1) :
   is_equiv (ab_qg_map H) :=
-proof is_equiv_qg_map _ h qed
+proof @is_equiv_qg_map G H (is_normal_subgroup_ab _) h qed
 
-definition ab_quotient_group_isomorphism [constructor] {G : AbGroup} (H : subgroup_rel G)
+definition ab_quotient_group_isomorphism [constructor] {G : AbGroup} (H : property G) [is_subgroup G H]
   (h : Πg, H g → g = 1) : quotient_ab_group H ≃g G :=
 (isomorphism.mk _ (is_equiv_ab_qg_map H h))⁻¹ᵍ
 
@@ -42,41 +44,38 @@ namespace left_module
 /- submodules -/
 variables {R : Ring} {M M₁ M₂ M₃ : LeftModule R} {m m₁ m₂ : M}
 
-structure submodule_rel (M : LeftModule R) : Type :=
-  (S : M → Prop)
-  (Szero : S 0)
-  (Sadd : Π⦃g h⦄, S g → S h → S (g + h))
-  (Ssmul : Π⦃g⦄ (r : R), S g → S (r • g))
+structure is_submodule [class] (M : LeftModule R) (S : property M) : Type :=
+  (zero_mem : 0 ∈ S)
+  (add_mem : Π⦃g h⦄, g ∈ S → h ∈ S → g + h ∈ S)
+  (smul_mem : Π⦃g⦄ (r : R), g ∈ S → r • g ∈ S)
 
-definition contains_zero := @submodule_rel.Szero
-definition contains_add  := @submodule_rel.Sadd
-definition contains_smul := @submodule_rel.Ssmul
-attribute submodule_rel.S [coercion]
+definition zero_mem {R : Ring} {M : LeftModule R} (S : property M) [is_submodule M S] := is_submodule.zero_mem S
+definition add_mem {R : Ring} {M : LeftModule R} (S : property M) [is_submodule M S] := @is_submodule.add_mem R M S
+definition smul_mem {R : Ring} {M : LeftModule R} (S : property M) [is_submodule M S] := @is_submodule.smul_mem R M S
 
-theorem contains_neg (S : submodule_rel M) ⦃m⦄ (H : S m) : S (-m) :=
-transport (λx, S x) (neg_one_smul m) (contains_smul S (- 1) H)
+theorem neg_mem (S : property M) [is_submodule M S] ⦃m⦄ (H : m ∈ S) : -m ∈ S :=
+transport (λx, x ∈ S) (neg_one_smul m) (smul_mem S (- 1) H)
 
-theorem is_normal_submodule (S : submodule_rel M) ⦃m₁ m₂⦄ (H : S m₁) : S (m₂ + m₁ + (-m₂)) :=
+theorem is_normal_submodule (S : property M) [is_submodule M S] ⦃m₁ m₂⦄ (H : S m₁) : S (m₂ + m₁ + (-m₂)) :=
 transport (λx, S x) (by rewrite [add.comm, neg_add_cancel_left]) H
 
-open submodule_rel
+-- open is_submodule
 
-variables {S : submodule_rel M}
+variables {S : property M} [is_submodule M S]
 
-definition subgroup_rel_of_submodule_rel [constructor] (S : submodule_rel M) :
-  subgroup_rel (AddGroup_of_AddAbGroup M) :=
-subgroup_rel.mk S (contains_zero S) (contains_add S) (contains_neg S)
+definition is_subgroup_of_is_submodule [instance] (S : property M) [is_submodule M S] :
+  is_subgroup (AddGroup_of_AddAbGroup M) S :=
+is_subgroup.mk (zero_mem S) (add_mem S) (neg_mem S)
 
-definition submodule_rel_of_subgroup_rel [constructor] (S : subgroup_rel (AddGroup_of_AddAbGroup M))
-  (h : Π⦃g⦄ (r : R), S g → S (r • g)) : submodule_rel M :=
-submodule_rel.mk S (subgroup_has_one S) @(subgroup_respect_mul S) h
+definition is_subgroup_of_is_submodule' [instance] (S : property M) [is_submodule M S] : is_subgroup (Group_of_AbGroup (AddAbGroup_of_LeftModule M)) S :=
+is_subgroup.mk (zero_mem S) (add_mem S) (neg_mem S)
 
-definition submodule' (S : submodule_rel M) : AddAbGroup :=
-ab_subgroup (subgroup_rel_of_submodule_rel S)
+definition submodule' (S : property M) [is_submodule M S] : AddAbGroup :=
+ab_subgroup S -- (subgroup_rel_of_submodule_rel S)
 
-definition submodule_smul [constructor] (S : submodule_rel M) (r : R) :
+definition submodule_smul [constructor] (S : property M) [is_submodule M S] (r : R) :
   submodule' S →a submodule' S :=
-ab_subgroup_functor (smul_homomorphism M r) (λg, contains_smul S r)
+ab_subgroup_functor (smul_homomorphism M r) (λg, smul_mem S r)
 
 definition submodule_smul_right_distrib (r s : R) (n : submodule' S) :
   submodule_smul S (r + s) n = submodule_smul S r n + submodule_smul S s n :=
@@ -96,148 +95,158 @@ definition submodule_mul_smul (r s : R) (n : submodule' S) :
   submodule_smul S (r * s) n = submodule_smul S r (submodule_smul S s n) :=
 by rexact submodule_mul_smul' r s n
 
-definition submodule_one_smul (n : submodule' S) : submodule_smul S 1 n = n :=
+definition submodule_one_smul (n : submodule' S) : submodule_smul S (1 : R) n = n :=
 begin
   refine subgroup_functor_homotopy _ _ _ n ⬝ !subgroup_functor_gid,
   intro m, exact to_one_smul m
 end
 
-definition submodule (S : submodule_rel M) : LeftModule R :=
+definition submodule (S : property M) [is_submodule M S] : LeftModule R :=
 LeftModule_of_AddAbGroup (submodule' S) (submodule_smul S)
   (λr, homomorphism.addstruct (submodule_smul S r))
   submodule_smul_right_distrib
   submodule_mul_smul
   submodule_one_smul
 
-definition submodule_incl [constructor] (S : submodule_rel M) : submodule S →lm M :=
+definition submodule_incl [constructor] (S : property M) [is_submodule M S] : submodule S →lm M :=
 lm_homomorphism_of_group_homomorphism (incl_of_subgroup _)
   begin
     intro r m, induction m with m hm, reflexivity
   end
 
-definition hom_lift [constructor] {K : submodule_rel M₂} (φ : M₁ →lm M₂)
-  (h : Π (m : M₁), K (φ m)) : M₁ →lm submodule K :=
+definition hom_lift [constructor] {K : property M₂} [is_submodule M₂ K] (φ : M₁ →lm M₂)
+  (h : Π (m : M₁), φ m ∈ K) : M₁ →lm submodule K :=
 lm_homomorphism_of_group_homomorphism (hom_lift (group_homomorphism_of_lm_homomorphism φ) _ h)
   begin
     intro r g, exact subtype_eq (to_respect_smul φ r g)
   end
 
-definition submodule_functor [constructor] {S : submodule_rel M₁} {K : submodule_rel M₂}
-  (φ : M₁ →lm M₂) (h : Π (m : M₁), S m → K (φ m)) : submodule S →lm submodule K :=
+definition submodule_functor [constructor] {S : property M₁} [is_submodule M₁ S]
+  {K : property M₂} [is_submodule M₂ K]
+  (φ : M₁ →lm M₂) (h : Π (m : M₁), m ∈ S → φ m ∈ K) : submodule S →lm submodule K :=
 hom_lift (φ ∘lm submodule_incl S) (by intro m; exact h m.1 m.2)
 
-definition hom_lift_compose {K : submodule_rel M₃}
-  (φ : M₂ →lm M₃) (h : Π (m : M₂), K (φ m)) (ψ : M₁ →lm M₂) :
+definition hom_lift_compose {K : property M₃} [is_submodule M₃ K]
+  (φ : M₂ →lm M₃) (h : Π (m : M₂), φ m ∈ K) (ψ : M₁ →lm M₂) :
   hom_lift φ h ∘lm ψ ~ hom_lift (φ ∘lm ψ) proof (λm, h (ψ m)) qed :=
 by reflexivity
 
-definition hom_lift_homotopy {K : submodule_rel M₂} {φ : M₁ →lm M₂}
-  {h : Π (m : M₁), K (φ m)} {φ' : M₁ →lm M₂}
-  {h' : Π (m : M₁), K (φ' m)} (p : φ ~ φ') : hom_lift φ h ~ hom_lift φ' h' :=
+definition hom_lift_homotopy {K : property M₂} [is_submodule M₂ K] {φ : M₁ →lm M₂}
+  {h : Π (m : M₁), φ m ∈ K} {φ' : M₁ →lm M₂}
+  {h' : Π (m : M₁), φ' m ∈ K} (p : φ ~ φ') : hom_lift φ h ~ hom_lift φ' h' :=
 λg, subtype_eq (p g)
 
-definition incl_smul (S : submodule_rel M) (r : R) (m : M) (h : S m) :
-  r • ⟨m, h⟩ = ⟨_, contains_smul S r h⟩ :> submodule S :=
+definition incl_smul (S : property M) [is_submodule M S] (r : R) (m : M) (h : S m) :
+  r • ⟨m, h⟩ = ⟨_, smul_mem S r h⟩ :> submodule S :=
 by reflexivity
 
-definition submodule_rel_submodule [constructor] (S₂ S₁ : submodule_rel M) :
-  submodule_rel (submodule S₂) :=
-submodule_rel.mk (λm, S₁ (submodule_incl S₂ m))
-  (contains_zero S₁)
-  (λm n p q, contains_add S₁ p q)
+definition property_submodule (S₁ S₂ : property M) [is_submodule M S₁] [is_submodule M S₂] :
+  property (submodule S₁) := {m | submodule_incl S₁ m ∈ S₂}
+
+definition is_submodule_property_submodule [instance] (S₁ S₂ : property M) [is_submodule M S₁] [is_submodule M S₂] :
+  is_submodule (submodule S₁) (property_submodule S₁ S₂) :=
+is_submodule.mk
+  (mem_property_of (zero_mem S₂))
+  (λm n p q, mem_property_of (add_mem S₂ (of_mem_property_of p) (of_mem_property_of q)))
   begin
-    intro m r p, induction m with m hm, exact contains_smul S₁ r p
+    intro m r p, induction m with m hm, apply mem_property_of,
+    apply smul_mem S₂, exact (of_mem_property_of p)
   end
 
-definition submodule_rel_submodule_trivial [constructor] {S₂ S₁ : submodule_rel M}
-  (h : Π⦃m⦄, S₁ m → m = 0) ⦃m : submodule S₂⦄ (Sm : submodule_rel_submodule S₂ S₁ m) : m = 0 :=
+definition eq_zero_of_mem_property_submodule_trivial [constructor] {S₁ S₂ : property M} [is_submodule M S₁] [is_submodule M S₂]
+  (h : Π⦃m⦄, m ∈ S₂ → m = 0) ⦃m : submodule S₁⦄ (Sm : m ∈ property_submodule S₁ S₂) : m = 0 :=
 begin
   fapply subtype_eq,
-  apply h Sm
+  apply h (of_mem_property_of Sm)
 end
 
-definition is_prop_submodule (S : submodule_rel M) [H : is_prop M] : is_prop (submodule S) :=
+definition is_prop_submodule (S : property M) [is_submodule M S] [H : is_prop M] : is_prop (submodule S) :=
 begin apply @is_trunc_sigma, exact H end
 local attribute is_prop_submodule [instance]
-definition is_contr_submodule [instance] (S : submodule_rel M) [is_contr M] : is_contr (submodule S) :=
+definition is_contr_submodule [instance] (S : property M) [is_submodule M S] [is_contr M] : is_contr (submodule S) :=
 is_contr_of_inhabited_prop 0
 
-definition submodule_isomorphism [constructor] (S : submodule_rel M) (h : Πg, S g) :
+definition submodule_isomorphism [constructor] (S : property M) [is_submodule M S] (h : Πg, g ∈ S) :
   submodule S ≃lm M :=
-isomorphism.mk (submodule_incl S) (is_equiv_incl_of_subgroup (subgroup_rel_of_submodule_rel S) h)
+isomorphism.mk (submodule_incl S) (is_equiv_incl_of_subgroup S h)
 
 /- quotient modules -/
 
-definition quotient_module' (S : submodule_rel M) : AddAbGroup :=
-quotient_ab_group (subgroup_rel_of_submodule_rel S)
+definition quotient_module' (S : property M) [is_submodule M S] : AddAbGroup :=
+quotient_ab_group S -- (subgroup_rel_of_submodule_rel S)
 
-definition quotient_module_smul [constructor] (S : submodule_rel M) (r : R) :
+definition quotient_module_smul [constructor] (S : property M) [is_submodule M S] (r : R) :
   quotient_module' S →a quotient_module' S :=
-quotient_ab_group_functor (smul_homomorphism M r) (λg, contains_smul S r)
-
-
+quotient_ab_group_functor (smul_homomorphism M r) (λg, smul_mem S r)
 
 definition quotient_module_smul_right_distrib (r s : R) (n : quotient_module' S) :
   quotient_module_smul S (r + s) n = quotient_module_smul S r n + quotient_module_smul S s n :=
 begin
-  refine quotient_group_functor_homotopy _ _ _ n ⬝ !quotient_group_functor_mul⁻¹,
+  refine quotient_ab_group_functor_homotopy _ _ _ n ⬝ !quotient_ab_group_functor_mul⁻¹,
   intro m, exact to_smul_right_distrib r s m
 end
 
 definition quotient_module_mul_smul' (r s : R) (n : quotient_module' S) :
   quotient_module_smul S (r * s) n = (quotient_module_smul S r ∘g quotient_module_smul S s) n :=
 begin
-  refine quotient_group_functor_homotopy _ _ _ n ⬝ (quotient_group_functor_compose _ _ _ _ n)⁻¹ᵖ,
-  intro m, exact to_mul_smul r s m
+  apply eq.symm,
+  apply eq.trans (quotient_ab_group_functor_compose _ _ _ _ n),
+  apply quotient_ab_group_functor_homotopy,
+  intro m, exact eq.symm (to_mul_smul r s m)
 end
+-- previous proof:
+--  refine quotient_ab_group_functor_homotopy _ _ _ n ⬝
+--    (quotient_ab_group_functor_compose (quotient_module_smul S r) (quotient_module_smul S s) _ _ n)⁻¹ᵖ,
+--  intro m, to_mul_smul r s m
 
 definition quotient_module_mul_smul (r s : R) (n : quotient_module' S) :
   quotient_module_smul S (r * s) n = quotient_module_smul S r (quotient_module_smul S s n) :=
 by rexact quotient_module_mul_smul' r s n
 
-definition quotient_module_one_smul (n : quotient_module' S) : quotient_module_smul S 1 n = n :=
+definition quotient_module_one_smul (n : quotient_module' S) : quotient_module_smul S (1 : R) n = n :=
 begin
-  refine quotient_group_functor_homotopy _ _ _ n ⬝ !quotient_group_functor_gid,
+  refine quotient_ab_group_functor_homotopy _ _ _ n ⬝ !quotient_ab_group_functor_gid,
   intro m, exact to_one_smul m
 end
 
-definition quotient_module (S : submodule_rel M) : LeftModule R :=
+definition quotient_module (S : property M) [is_submodule M S] : LeftModule R :=
 LeftModule_of_AddAbGroup (quotient_module' S) (quotient_module_smul S)
   (λr, homomorphism.addstruct (quotient_module_smul S r))
   quotient_module_smul_right_distrib
   quotient_module_mul_smul
   quotient_module_one_smul
 
-definition quotient_map [constructor] (S : submodule_rel M) : M →lm quotient_module S :=
+definition quotient_map [constructor] (S : property M) [is_submodule M S] : M →lm quotient_module S :=
 lm_homomorphism_of_group_homomorphism (ab_qg_map _) (λr g, idp)
 
 definition quotient_map_eq_zero (m : M) (H : S m) : quotient_map S m = 0 :=
-qg_map_eq_one _ H
+@qg_map_eq_one _ _ (is_normal_subgroup_ab _) _ H
 
 definition rel_of_quotient_map_eq_zero (m : M) (H : quotient_map S m = 0) : S m :=
-rel_of_qg_map_eq_one m H
+@rel_of_qg_map_eq_one _ _ (is_normal_subgroup_ab _) m H
 
-definition quotient_elim [constructor] (φ : M →lm M₂) (H : Π⦃m⦄, S m → φ m = 0) :
+definition quotient_elim [constructor] (φ : M →lm M₂) (H : Π⦃m⦄, m ∈ S → φ m = 0) :
   quotient_module S →lm M₂ :=
 lm_homomorphism_of_group_homomorphism
-  (quotient_group_elim (group_homomorphism_of_lm_homomorphism φ) H)
+  (quotient_ab_group_elim (group_homomorphism_of_lm_homomorphism φ) H)
   begin
-    intro r m, esimp,
-    induction m using set_quotient.rec_prop with m,
+    intro r, esimp,
+    refine @set_quotient.rec_prop _ _ _ (λ x, !is_trunc_eq) _,
+    intro m,
     exact to_respect_smul φ r m
   end
 
-definition is_prop_quotient_module (S : submodule_rel M) [H : is_prop M] : is_prop (quotient_module S) :=
+definition is_prop_quotient_module (S : property M) [is_submodule M S] [H : is_prop M] : is_prop (quotient_module S) :=
 begin apply @set_quotient.is_trunc_set_quotient, exact H end
 local attribute is_prop_quotient_module [instance]
 
-definition is_contr_quotient_module [instance] (S : submodule_rel M) [is_contr M] :
+definition is_contr_quotient_module [instance] (S : property M) [is_submodule M S] [is_contr M] :
   is_contr (quotient_module S) :=
 is_contr_of_inhabited_prop 0
 
-definition quotient_module_isomorphism [constructor] (S : submodule_rel M) (h : Π⦃m⦄, S m → m = 0) :
+definition quotient_module_isomorphism [constructor] (S : property M) [is_submodule M S] (h : Π⦃m⦄, S m → m = 0) :
   quotient_module S ≃lm M :=
-(isomorphism.mk (quotient_map S) (is_equiv_ab_qg_map (subgroup_rel_of_submodule_rel S) h))⁻¹ˡᵐ
+(isomorphism.mk (quotient_map S) (is_equiv_ab_qg_map S h))⁻¹ˡᵐ
 
 /- specific submodules -/
 definition has_scalar_image (φ : M₁ →lm M₂) ⦃m : M₂⦄ (r : R)
@@ -248,12 +257,26 @@ begin
   refine to_respect_smul φ r m' ⬝ ap (λx, r • x) p,
 end
 
+definition is_submodule_image [instance] (φ : M₁ →lm M₂) : is_submodule M₂ (image φ) :=
+is_submodule.mk
+  (show 0 ∈ image (group_homomorphism_of_lm_homomorphism φ),
+    begin apply is_subgroup.one_mem, apply is_subgroup_image end)
+  (λ g₁ g₂ hg₁ hg₂,
+     show g₁ + g₂ ∈ image (group_homomorphism_of_lm_homomorphism φ),
+     begin
+       apply @is_subgroup.mul_mem,
+       apply is_subgroup_image, exact hg₁, exact hg₂
+     end)
+  (has_scalar_image φ)
+
+/-
 definition image_rel [constructor] (φ : M₁ →lm M₂) : submodule_rel M₂ :=
 submodule_rel_of_subgroup_rel
   (image_subgroup (group_homomorphism_of_lm_homomorphism φ))
   (has_scalar_image φ)
+-/
 
-definition image_rel_trivial (φ : M₁ →lm M₂) [H : is_contr M₁] ⦃m : M₂⦄ (h : image_rel φ m) : m = 0 :=
+definition image_trivial (φ : M₁ →lm M₂) [H : is_contr M₁] ⦃m : M₂⦄ (h : m ∈ image φ) : m = 0 :=
 begin
   refine image.rec _ h,
   intro x p,
@@ -261,7 +284,7 @@ begin
   apply @is_prop.elim, apply is_trunc_succ, exact H
 end
 
-definition image_module [constructor] (φ : M₁ →lm M₂) : LeftModule R := submodule (image_rel φ)
+definition image_module [constructor] (φ : M₁ →lm M₂) : LeftModule R := submodule (image φ)
 
 -- unfortunately this is note definitionally equal:
 -- definition foo (φ : M₁ →lm M₂) :
@@ -281,7 +304,9 @@ variables {ψ : M₂ →lm M₃} {φ : M₁ →lm M₂} {θ : M₁ →lm M₃}
 definition image_elim [constructor] (θ : M₁ →lm M₃) (h : Π⦃g⦄, φ g = 0 → θ g = 0) :
   image_module φ →lm M₃ :=
 begin
-  refine homomorphism.mk (image_elim (group_homomorphism_of_lm_homomorphism θ) h) _,
+  fapply homomorphism.mk,
+  change Image (group_homomorphism_of_lm_homomorphism φ) → M₃,
+  exact image_elim (group_homomorphism_of_lm_homomorphism θ) h,
   split,
   { exact homomorphism.struct (image_elim (group_homomorphism_of_lm_homomorphism θ) _) },
   { intro r, refine @total_image.rec _ _ _ _ (λx, !is_trunc_eq) _, intro g,
@@ -304,7 +329,7 @@ definition is_contr_image_module [instance] (φ : M₁ →lm M₂) [is_contr M
   is_contr (image_module φ) :=
 !is_contr_submodule
 
-definition is_contr_image_module_of_is_contr_dom (φ : M₁ →lm M₂) [is_contr M₁] :
+definition is_contr_image_module_of_is_contr_dom (φ : M₁ →lm M₂) [is_contrM₁ : is_contr M₁] :
   is_contr (image_module φ) :=
 is_contr.mk 0
   begin
@@ -312,7 +337,8 @@ is_contr.mk 0
     apply @total_image.rec,
     exact this,
     intro m,
-    induction (is_prop.elim 0 m), apply subtype_eq,
+    have h : is_contr (LeftModule.carrier M₁), from is_contrM₁,
+    induction (eq_of_is_contr 0 m), apply subtype_eq,
     exact (to_respect_zero φ)⁻¹
   end
 
@@ -326,28 +352,41 @@ begin
   refine to_respect_smul φ r m ⬝ ap (λx, r • x) p ⬝ smul_zero r,
 end
 
-definition kernel_rel [constructor] (φ : M₁ →lm M₂) : submodule_rel M₁ :=
-submodule_rel_of_subgroup_rel
-  (kernel_subgroup (group_homomorphism_of_lm_homomorphism φ))
+definition lm_kernel [reducible] (φ : M₁ →lm M₂) : property M₁ := kernel (group_homomorphism_of_lm_homomorphism φ)
+
+definition is_submodule_kernel [instance] (φ : M₁ →lm M₂) : is_submodule M₁ (lm_kernel φ) :=
+is_submodule.mk
+  (show 0 ∈ kernel (group_homomorphism_of_lm_homomorphism φ),
+    begin apply is_subgroup.one_mem, apply is_subgroup_kernel end)
+  (λ g₁ g₂ hg₁ hg₂,
+     show g₁ + g₂ ∈ kernel (group_homomorphism_of_lm_homomorphism φ),
+       begin apply @is_subgroup.mul_mem, apply is_subgroup_kernel, exact hg₁, exact hg₂ end)
   (has_scalar_kernel φ)
 
-definition kernel_rel_full (φ : M₁ →lm M₂) [is_contr M₂] (m : M₁) : kernel_rel φ m :=
+definition kernel_full (φ : M₁ →lm M₂) [is_contr M₂] (m : M₁) : m ∈ lm_kernel φ :=
 !is_prop.elim
 
-definition kernel_module [constructor] (φ : M₁ →lm M₂) : LeftModule R := submodule (kernel_rel φ)
+definition kernel_module [reducible] (φ : M₁ →lm M₂) : LeftModule R := submodule (lm_kernel φ)
 
 definition is_contr_kernel_module [instance] (φ : M₁ →lm M₂) [is_contr M₁] :
   is_contr (kernel_module φ) :=
 !is_contr_submodule
 
 definition kernel_module_isomorphism [constructor] (φ : M₁ →lm M₂) [is_contr M₂] : kernel_module φ ≃lm M₁ :=
-submodule_isomorphism _ (kernel_rel_full φ)
+submodule_isomorphism _ (kernel_full φ)
+
+definition homology_quotient_property (ψ : M₂ →lm M₃) (φ : M₁ →lm M₂) : property (kernel_module ψ) :=
+property_submodule (lm_kernel ψ) (image (homomorphism_fn φ))
+
+definition is_submodule_homology_property [instance] (ψ : M₂ →lm M₃) (φ : M₁ →lm M₂) :
+  is_submodule (kernel_module ψ) (homology_quotient_property ψ φ) :=
+(is_submodule_property_submodule _ (image φ))
 
 definition homology (ψ : M₂ →lm M₃) (φ : M₁ →lm M₂) : LeftModule R :=
-@quotient_module R (submodule (kernel_rel ψ)) (submodule_rel_submodule _ (image_rel φ))
+quotient_module (homology_quotient_property ψ φ)
 
 definition homology.mk (φ : M₁ →lm M₂) (m : M₂) (h : ψ m = 0) : homology ψ φ :=
-quotient_map _ ⟨m, h⟩
+quotient_map (homology_quotient_property ψ φ) ⟨m, h⟩
 
 definition homology_eq0 {m : M₂} {hm : ψ m = 0} (h : image φ m) :
   homology.mk φ m hm = 0 :=
@@ -368,8 +407,8 @@ quotient_elim (θ ∘lm submodule_incl _)
     intro m x,
     induction m with m h,
     esimp at *,
-    induction x with v, induction v with m' p,
-    exact ap θ p⁻¹ ⬝ H m'
+    induction x with v,
+    exact ap θ p⁻¹ ⬝ H v -- m'
   end
 
 definition is_contr_homology [instance] (ψ : M₂ →lm M₃) (φ : M₁ →lm M₂) [is_contr M₂] :
@@ -378,8 +417,8 @@ begin apply @is_contr_quotient_module end
 
 definition homology_isomorphism [constructor] (ψ : M₂ →lm M₃) (φ : M₁ →lm M₂)
   [is_contr M₁] [is_contr M₃] : homology ψ φ ≃lm M₂ :=
-quotient_module_isomorphism _ (submodule_rel_submodule_trivial (image_rel_trivial φ)) ⬝lm
-!kernel_module_isomorphism
+(quotient_module_isomorphism (homology_quotient_property ψ φ)
+  (eq_zero_of_mem_property_submodule_trivial (image_trivial _))) ⬝lm (kernel_module_isomorphism ψ)
 
 -- remove:
 
diff --git a/homotopy/EM.hlean b/homotopy/EM.hlean
index 29a642f..474b716 100644
--- a/homotopy/EM.hlean
+++ b/homotopy/EM.hlean
@@ -626,7 +626,7 @@ namespace EM
   /- TODO: other cases -/
   definition LES_isomorphism_kernel_of_trivial.{u}
     {X Y : pType.{u}} (f : X →* Y) (n : ℕ) [H : is_succ n]
-    (H1 : is_contr (πg[n+1] Y)) : πg[n] (pfiber f) ≃g kernel (π→g[n] f) :=
+    (H1 : is_contr (πg[n+1] Y)) : πg[n] (pfiber f) ≃g Kernel (π→g[n] f) :=
   begin
     induction H with n,
     have H2 : is_exact (π→g[n+1] (ppoint f)) (π→g[n+1] f),
@@ -641,7 +641,7 @@ namespace EM
 
   open group algebra is_trunc
   definition homotopy_group_fiber_EM1_functor.{u} {G H : Group.{u}} (φ : G →g H) :
-    π₁ (pfiber (EM1_functor φ)) ≃g kernel φ :=
+    π₁ (pfiber (EM1_functor φ)) ≃g Kernel φ :=
   have H1 : is_trunc 1 (EM1 H), from sorry,
   have H2 : 1 <[ℕ] 1 + 1, from sorry,
   LES_isomorphism_kernel_of_trivial (EM1_functor φ) 1
@@ -649,12 +649,12 @@ namespace EM
   sorry
 
   definition homotopy_group_fiber_EMadd1_functor {G H : AbGroup} (φ : G →g H) (n : ℕ) :
-    πg[n+1] (pfiber (EMadd1_functor φ n)) ≃g kernel φ :=
+    πg[n+1] (pfiber (EMadd1_functor φ n)) ≃g Kernel φ :=
   sorry
 
   /- TODO: move-/
   definition cokernel {G H : AbGroup} (φ : G →g H) : AbGroup :=
-  quotient_ab_group (image_subgroup φ)
+  quotient_ab_group (image φ)
 
   definition trunc_fiber_EM1_functor {G H : Group} (φ : G →g H) :
     ptrunc 0 (pfiber (EM1_functor φ)) ≃* sorry :=
diff --git a/property.hlean b/property.hlean
index b6a313a..65213a1 100644
--- a/property.hlean
+++ b/property.hlean
@@ -105,6 +105,154 @@ theorem eq_univ_of_forall {s : property X} (H : ∀ x, x ∈ s) : s = univ :=
 ext (take x, iff.intro (assume H', trivial) (assume H', H x))
 -/
 
+/- union -/
+
+definition union (a b : property X) : property X := λx, x ∈ a ∨ x ∈ b
+notation a ∪ b := union a b
+
+theorem mem_union_left {x : X} {a : property X} (b : property X) : x ∈ a → x ∈ a ∪ b :=
+assume h, or.inl h
+
+theorem mem_union_right {x : X} {b : property X} (a : property X) : x ∈ b → x ∈ a ∪ b :=
+assume h, or.inr h
+
+theorem mem_unionl {x : X} {a b : property X} : x ∈ a → x ∈ a ∪ b :=
+assume h, or.inl h
+
+theorem mem_unionr {x : X} {a b : property X} : x ∈ b → x ∈ a ∪ b :=
+assume h, or.inr h
+
+theorem mem_or_mem_of_mem_union {x : X} {a b : property X} (H : x ∈ a ∪ b) : x ∈ a ∨ x ∈ b := H
+
+theorem mem_union.elim {x : X} {a b : property X} {P : Prop}
+    (H₁ : x ∈ a ∪ b) (H₂ : x ∈ a → P) (H₃ : x ∈ b → P) : P :=
+or.elim H₁ H₂ H₃
+
+theorem mem_union_iff (x : X) (a b : property X) : x ∈ a ∪ b ↔ x ∈ a ∨ x ∈ b := !iff.refl
+
+theorem mem_union_eq (x : X) (a b : property X) : x ∈ a ∪ b = (x ∈ a ∨ x ∈ b) := rfl
+
+--theorem union_self (a : property X) : a ∪ a = a :=
+--ext (take x, !or_self)
+
+--theorem union_empty (a : property X) : a ∪ ∅ = a :=
+--ext (take x, !or_false)
+
+--theorem empty_union (a : property X) : ∅ ∪ a = a :=
+--ext (take x, !false_or)
+
+--theorem union_comm (a b : property X) : a ∪ b = b ∪ a :=
+--ext (take x, or.comm)
+
+--theorem union_assoc (a b c : property X) : (a ∪ b) ∪ c = a ∪ (b ∪ c) :=
+--ext (take x, or.assoc)
+
+--theorem union_left_comm (s₁ s₂ s₃ : property X) : s₁ ∪ (s₂ ∪ s₃) = s₂ ∪ (s₁ ∪ s₃) :=
+--!left_comm union_comm union_assoc s₁ s₂ s₃
+
+--theorem union_right_comm (s₁ s₂ s₃ : property X) : (s₁ ∪ s₂) ∪ s₃ = (s₁ ∪ s₃) ∪ s₂ :=
+--!right_comm union_comm union_assoc s₁ s₂ s₃
+
+theorem subproperty_union_left (s t : property X) : s ⊆ s ∪ t := λ x H, or.inl H
+
+theorem subproperty_union_right (s t : property X) : t ⊆ s ∪ t := λ x H, or.inr H
+
+theorem union_subproperty {s t r : property X} (sr : s ⊆ r) (tr : t ⊆ r) : s ∪ t ⊆ r :=
+λ x xst, or.elim xst (λ xs, sr xs) (λ xt, tr xt)
+
+/- intersection -/
+
+definition inter (a b : property X) : property X := λx, x ∈ a ∧ x ∈ b
+notation a ∩ b := inter a b
+
+theorem mem_inter_iff (x : X) (a b : property X) : x ∈ a ∩ b ↔ x ∈ a ∧ x ∈ b := !iff.refl
+
+theorem mem_inter_eq (x : X) (a b : property X) : x ∈ a ∩ b = (x ∈ a ∧ x ∈ b) := rfl
+
+theorem mem_inter {x : X} {a b : property X} (Ha : x ∈ a) (Hb : x ∈ b) : x ∈ a ∩ b :=
+and.intro Ha Hb
+
+theorem mem_of_mem_inter_left {x : X} {a b : property X} (H : x ∈ a ∩ b) : x ∈ a :=
+and.left H
+
+theorem mem_of_mem_inter_right {x : X} {a b : property X} (H : x ∈ a ∩ b) : x ∈ b :=
+and.right H
+
+--theorem inter_self (a : property X) : a ∩ a = a :=
+--ext (take x, !and_self)
+
+--theorem inter_empty (a : property X) : a ∩ ∅ = ∅ :=
+--ext (take x, !and_false)
+
+--theorem empty_inter (a : property X) : ∅ ∩ a = ∅ :=
+--ext (take x, !false_and)
+
+--theorem nonempty_of_inter_nonempty_right {T : Type} {s t : property T} (H : s ∩ t ≠ ∅) : t ≠ ∅ :=
+--suppose t = ∅,
+--have s ∩ t = ∅, by rewrite this; apply inter_empty,
+--H this
+
+--theorem nonempty_of_inter_nonempty_left {T : Type} {s t : property T} (H : s ∩ t ≠ ∅) : s ≠ ∅ :=
+--suppose s = ∅,
+--have s ∩ t = ∅, by rewrite this; apply empty_inter,
+--H this
+
+--theorem inter_comm (a b : property X) : a ∩ b = b ∩ a :=
+--ext (take x, !and.comm)
+
+--theorem inter_assoc (a b c : property X) : (a ∩ b) ∩ c = a ∩ (b ∩ c) :=
+--ext (take x, !and.assoc)
+
+--theorem inter_left_comm (s₁ s₂ s₃ : property X) : s₁ ∩ (s₂ ∩ s₃) = s₂ ∩ (s₁ ∩ s₃) :=
+--!left_comm inter_comm inter_assoc s₁ s₂ s₃
+
+--theorem inter_right_comm (s₁ s₂ s₃ : property X) : (s₁ ∩ s₂) ∩ s₃ = (s₁ ∩ s₃) ∩ s₂ :=
+--!right_comm inter_comm inter_assoc s₁ s₂ s₃
+
+--theorem inter_univ (a : property X) : a ∩ univ = a :=
+--ext (take x, !and_true)
+
+--theorem univ_inter (a : property X) : univ ∩ a = a :=
+--ext (take x, !true_and)
+
+theorem inter_subproperty_left (s t : property X) : s ∩ t ⊆ s := λ x H, and.left H
+
+theorem inter_subproperty_right (s t : property X) : s ∩ t ⊆ t := λ x H, and.right H
+
+theorem inter_subproperty_inter_right {s t : property X} (u : property X) (H : s ⊆ t) : s ∩ u ⊆ t ∩ u :=
+take x, assume xsu, and.intro (H (and.left xsu)) (and.right xsu)
+
+theorem inter_subproperty_inter_left {s t : property X} (u : property X) (H : s ⊆ t) : u ∩ s ⊆ u ∩ t :=
+take x, assume xus, and.intro (and.left xus) (H (and.right xus))
+
+theorem subproperty_inter {s t r : property X} (rs : r ⊆ s) (rt : r ⊆ t) : r ⊆ s ∩ t :=
+λ x xr, and.intro (rs xr) (rt xr)
+
+--theorem not_mem_of_mem_of_not_mem_inter_left {s t : property X} {x : X} (Hxs : x ∈ s) (Hnm : x ∉ s ∩ t) : x ∉ t :=
+--  suppose x ∈ t,
+--  have x ∈ s ∩ t, from and.intro Hxs this,
+--  show false, from Hnm this
+
+--theorem not_mem_of_mem_of_not_mem_inter_right {s t : property X} {x : X} (Hxs : x ∈ t) (Hnm : x ∉ s ∩ t) : x ∉ s :=
+--  suppose x ∈ s,
+--  have x ∈ s ∩ t, from and.intro this Hxs,
+--  show false, from Hnm this
+
+/- distributivity laws -/
+
+--theorem inter_distrib_left (s t u : property X) : s ∩ (t ∪ u) = (s ∩ t) ∪ (s ∩ u) :=
+--ext (take x, !and.left_distrib)
+
+--theorem inter_distrib_right (s t u : property X) : (s ∪ t) ∩ u = (s ∩ u) ∪ (t ∩ u) :=
+--ext (take x, !and.right_distrib)
+
+--theorem union_distrib_left (s t u : property X) : s ∪ (t ∩ u) = (s ∪ t) ∩ (s ∪ u) :=
+--ext (take x, !or.left_distrib)
+
+--theorem union_distrib_right (s t u : property X) : (s ∩ t) ∪ u = (s ∪ u) ∩ (t ∪ u) :=
+--ext (take x, !or.right_distrib)
+
+
 /- property-builder notation -/
 
 -- {x : X | P}