diff --git a/algebra/graded.hlean b/algebra/graded.hlean
index 78c53d9..4d41328 100644
--- a/algebra/graded.hlean
+++ b/algebra/graded.hlean
@@ -2,9 +2,9 @@
 
 -- Author: Floris van Doorn
 
-import .left_module .direct_sum
+import .left_module .direct_sum .submodule
 
-open algebra eq left_module pointed function equiv is_equiv is_trunc prod group
+open algebra eq left_module pointed function equiv is_equiv is_trunc prod group sigma
 
 namespace left_module
 
@@ -32,43 +32,81 @@ variables {R : Ring} {I : Type} {M M₁ M₂ M₃ : graded_module R I}
     deg f i = j
     we get a function M₁ i → M₂ j.
 -/
+
+definition graded_hom_of_deg (d : I ≃ I) (M₁ M₂ : graded_module R I) : Type :=
+Π⦃i j : I⦄ (p : d i = j), M₁ i →lm M₂ j
+
+definition gmd_constant [constructor] (d : I ≃ I) (M₁ M₂ : graded_module R I) : graded_hom_of_deg d M₁ M₂ :=
+λi j p, lm_constant (M₁ i) (M₂ j)
+
+definition gmd0 [constructor] {d : I ≃ I} {M₁ M₂ : graded_module R I} : graded_hom_of_deg d M₁ M₂ :=
+gmd_constant d M₁ M₂
+
 structure graded_hom (M₁ M₂ : graded_module R I) : Type :=
-mk' ::  (d : I → I)
-        (fn' : Π⦃i j : I⦄ (p : d i = j), M₁ i →lm M₂ j)
+mk' ::  (d : I ≃ I)
+        (fn' : graded_hom_of_deg d M₁ M₂)
 
 notation M₁ ` →gm ` M₂ := graded_hom M₁ M₂
 
 abbreviation deg [unfold 5] := @graded_hom.d
-notation `↘` := graded_hom.fn' -- there is probably a better character for this?
+postfix ` ↘`:(max+10) := graded_hom.fn' -- there is probably a better character for this? Maybe ↷?
 
-definition graded_hom_fn [unfold 5] [coercion] (f : M₁ →gm M₂) (i : I) : M₁ i →lm M₂ (deg f i) :=
-↘f idp
+definition graded_hom_fn [reducible] [unfold 5] [coercion] (f : M₁ →gm M₂) (i : I) : M₁ i →lm M₂ (deg f i) :=
+f ↘ idp
 
-definition graded_hom.mk [constructor] {M₁ M₂ : graded_module R I} (d : I → I)
+definition graded_hom_fn_in [reducible] [unfold 5] (f : M₁ →gm M₂) (i : I) : M₁ ((deg f)⁻¹ i) →lm M₂ i :=
+f ↘ (to_right_inv (deg f) i)
+
+infix ` ← `:101 := graded_hom_fn_in -- todo: change notation
+
+definition graded_hom.mk [constructor] {M₁ M₂ : graded_module R I} (d : I ≃ I)
   (fn : Πi, M₁ i →lm M₂ (d i)) : M₁ →gm M₂ :=
 graded_hom.mk' d (λi j p, homomorphism_of_eq (ap M₂ p) ∘lm fn i)
 
-variables {f' : M₂ →gm M₃} {f : M₁ →gm M₂}
+definition graded_hom.mk_in [constructor] {M₁ M₂ : graded_module R I} (d : I ≃ I)
+  (fn : Πi, M₁ (d⁻¹ i) →lm M₂ i) : M₁ →gm M₂ :=
+graded_hom.mk' d (λi j p, fn j ∘lm homomorphism_of_eq (ap M₁ (eq_inv_of_eq p)))
+
+definition graded_hom.mk_out_in [constructor] {M₁ M₂ : graded_module R I} (d₁ : I ≃ I) (d₂ : I ≃ I)
+  (fn : Πi, M₁ (d₁ i) →lm M₂ (d₂ i)) : M₁ →gm M₂ :=
+graded_hom.mk' (d₁⁻¹ᵉ ⬝e d₂) (λi j p, homomorphism_of_eq (ap M₂ p) ∘lm fn (d₁⁻¹ᵉ i) ∘lm
+  homomorphism_of_eq (ap M₁ (to_right_inv d₁ i)⁻¹))
+
+definition graded_hom_eq_transport (f : M₁ →gm M₂) {i j : I} (p : deg f i = j) (m : M₁ i) :
+  f ↘ p m = transport M₂ p (f i m) :=
+by induction p; reflexivity
+
+definition graded_hom_eq_zero {f : M₁ →gm M₂} {i j k : I} {q : deg f i = j} {p : deg f i = k}
+  (m : M₁ i) (r : f ↘ q m = 0) : f ↘ p m = 0 :=
+have f ↘ p m = transport M₂ (q⁻¹ ⬝ p) (f ↘ q m), begin induction p, induction q, reflexivity end,
+this ⬝ ap (transport M₂ (q⁻¹ ⬝ p)) r ⬝ tr_eq_of_pathover (apd (λi, 0) (q⁻¹ ⬝ p))
+
+variables {f' : M₂ →gm M₃} {f g : M₁ →gm M₂}
 
 definition graded_hom_compose [constructor] (f' : M₂ →gm M₃) (f : M₁ →gm M₂) : M₁ →gm M₃ :=
-graded_hom.mk (deg f' ∘ deg f) (λi, f' (deg f i) ∘lm f i)
+graded_hom.mk (deg f ⬝e deg f') (λi, f' (deg f i) ∘lm f i)
+
+infixr ` ∘gm `:75 := graded_hom_compose
+
+definition graded_hom_compose_fn (f' : M₂ →gm M₃) (f : M₁ →gm M₂) (i : I) (m : M₁ i) :
+  (f' ∘gm f) i m = f' (deg f i) (f i m) :=
+proof idp qed
 
 variable (M)
 definition graded_hom_id [constructor] [refl] : M →gm M :=
-graded_hom.mk id (λi, lmid)
+graded_hom.mk erfl (λi, lmid)
 variable {M}
-
 abbreviation gmid [constructor] := graded_hom_id M
-infixr ` ∘gm `:75 := graded_hom_compose
+
+definition gm_constant [constructor] (M₁ M₂ : graded_module R I) (d : I ≃ I) : M₁ →gm M₂ :=
+graded_hom.mk' d (gmd_constant d M₁ M₂)
 
 structure graded_iso (M₁ M₂ : graded_module R I) : Type :=
-  (to_hom : M₁ →gm M₂)
-  (is_equiv_deg : is_equiv (deg to_hom))
-  (is_equiv_to_hom : Π⦃i j⦄ (p : deg to_hom i = j), is_equiv (↘to_hom p))
+mk' :: (to_hom : M₁ →gm M₂)
+       (is_equiv_to_hom : Π⦃i j⦄ (p : deg to_hom i = j), is_equiv (to_hom ↘ p))
 
 infix ` ≃gm `:25 := graded_iso
 attribute graded_iso.to_hom [coercion]
-attribute graded_iso.is_equiv_deg [instance] [priority 1010]
 attribute graded_iso._trans_of_to_hom [unfold 5]
 
 definition is_equiv_graded_iso [instance] [priority 1010] (φ : M₁ ≃gm M₂) (i : I) :
@@ -77,59 +115,55 @@ graded_iso.is_equiv_to_hom φ idp
 
 definition isomorphism_of_graded_iso' [constructor] (φ : M₁ ≃gm M₂) {i j : I} (p : deg φ i = j) :
   M₁ i ≃lm M₂ j :=
-isomorphism.mk (↘φ p) !graded_iso.is_equiv_to_hom
+isomorphism.mk (φ ↘ p) !graded_iso.is_equiv_to_hom
 
 definition isomorphism_of_graded_iso [constructor] (φ : M₁ ≃gm M₂) (i : I) :
   M₁ i ≃lm M₂ (deg φ i) :=
 isomorphism.mk (φ i) _
 
-definition graded_iso_of_isomorphism [constructor] (d : I ≃ I) (φ : Πi, M₁ i ≃lm M₂ (d i)) :
+definition isomorphism_of_graded_iso_in [constructor] (φ : M₁ ≃gm M₂) (i : I) :
+  M₁ ((deg φ)⁻¹ i) ≃lm M₂ i :=
+isomorphism_of_graded_iso' φ !to_right_inv
+
+protected definition graded_iso.mk [constructor] (d : I ≃ I) (φ : Πi, M₁ i ≃lm M₂ (d i)) :
   M₁ ≃gm M₂ :=
 begin
-  apply graded_iso.mk (graded_hom.mk d φ), apply to_is_equiv, intro i j p, induction p,
+  apply graded_iso.mk' (graded_hom.mk d φ),
+  intro i j p, induction p,
   exact to_is_equiv (equiv_of_isomorphism (φ i)),
 end
 
+protected definition graded_iso.mk_in [constructor] (d : I ≃ I) (φ : Πi, M₁ (d⁻¹ i) ≃lm M₂ i) :
+  M₁ ≃gm M₂ :=
+begin
+  apply graded_iso.mk' (graded_hom.mk_in d φ),
+  intro i j p, esimp,
+  exact @is_equiv_compose _ _ _ _ _ !is_equiv_cast _,
+end
+
 definition graded_iso_of_eq [constructor] {M₁ M₂ : graded_module R I} (p : M₁ ~ M₂)
   : M₁ ≃gm M₂ :=
-graded_iso_of_isomorphism erfl (λi, isomorphism_of_eq (p i))
+graded_iso.mk erfl (λi, isomorphism_of_eq (p i))
 
--- definition graded_iso.MK [constructor] (d : I ≃ I) (fn : Πi, M₁ i →lm M₂ (d i))
---   : M₁ ≃gm M₂ :=
--- graded_iso.mk _ _ _ --d (λi j p, homomorphism_of_eq (ap M₂ p) ∘lm fn i)
-
-definition isodeg [unfold 5] (φ : M₁ ≃gm M₂) : I ≃ I :=
-equiv.mk (deg φ) _
-
-definition graded_iso_to_lminv [constructor] (φ : M₁ ≃gm M₂) : M₂ →gm M₁ :=
-graded_hom.mk (deg φ)⁻¹
-  abstract begin
-    intro i, apply to_lminv,
-    apply isomorphism_of_graded_iso' φ,
-    apply to_right_inv (isodeg φ) i
-  end end
-
-definition to_gminv [constructor] (φ : M₁ ≃gm M₂) : M₂ →gm M₁ :=
-graded_hom.mk (deg φ)⁻¹
-  abstract begin
-    intro i, apply isomorphism.to_hom, symmetry,
-    apply isomorphism_of_graded_iso' φ,
-    apply to_right_inv (isodeg φ) i
-  end end
+-- definition to_gminv [constructor] (φ : M₁ ≃gm M₂) : M₂ →gm M₁ :=
+-- graded_hom.mk_in (deg φ)⁻¹ᵉ
+--   abstract begin
+--     intro i, apply isomorphism.to_hom, symmetry,
+--     apply isomorphism_of_graded_iso φ
+--   end end
 
 variable (M)
 definition graded_iso.refl [refl] [constructor] : M ≃gm M :=
-graded_iso_of_isomorphism equiv.rfl (λi, isomorphism.rfl)
+graded_iso.mk equiv.rfl (λi, isomorphism.rfl)
 variable {M}
 
 definition graded_iso.rfl [refl] [constructor] : M ≃gm M := graded_iso.refl M
 
 definition graded_iso.symm [symm] [constructor] (φ : M₁ ≃gm M₂) : M₂ ≃gm M₁ :=
-graded_iso.mk (to_gminv φ) !is_equiv_inv
-  (λi j p, @is_equiv_compose _ _ _ _ _ !isomorphism.is_equiv_to_hom !is_equiv_cast)
+graded_iso.mk_in (deg φ)⁻¹ᵉ (λi, (isomorphism_of_graded_iso φ i)⁻¹ˡᵐ)
 
 definition graded_iso.trans [trans] [constructor] (φ : M₁ ≃gm M₂) (ψ : M₂ ≃gm M₃) : M₁ ≃gm M₃ :=
-graded_iso_of_isomorphism (isodeg φ ⬝e isodeg ψ)
+graded_iso.mk (deg φ ⬝e deg ψ)
   (λi, isomorphism_of_graded_iso φ i ⬝lm isomorphism_of_graded_iso ψ (deg φ i))
 
 definition graded_iso.eq_trans [trans] [constructor]
@@ -149,6 +183,63 @@ definition graded_hom_of_eq [constructor] {M₁ M₂ : graded_module R I} (p : M
   : M₁ →gm M₂ :=
 graded_iso_of_eq p
 
+structure graded_homotopy (f g : M₁ →gm M₂) : Type :=
+mk' :: (hd : deg f ~ deg g)
+       (hfn : Π⦃i j : I⦄ (pf : deg f i = j) (pg : deg g i = j) (r : hd i ⬝ pg = pf), f ↘ pf ~ g ↘ pg)
+
+infix ` ~gm `:50 := graded_homotopy
+
+definition graded_homotopy.mk (hd : deg f ~ deg g) (hfn : Πi m, f i m =[hd i] g i m) : f ~gm g :=
+graded_homotopy.mk' hd
+  begin
+    intro i j pf pg r m, induction r, induction pg, esimp,
+    exact graded_hom_eq_transport f (hd i) m ⬝ tr_eq_of_pathover (hfn i m),
+  end
+
+definition graded_homotopy_of_deg (d : I ≃ I) (f g : graded_hom_of_deg d M₁ M₂) : Type :=
+Π⦃i j : I⦄ (p : d i = j), f p ~ g p
+
+notation f ` ~[`:50 d:0 `] `:0 g:50 := graded_homotopy_of_deg d f g
+
+variables {d : I ≃ I} {f₁ f₂ : graded_hom_of_deg d M₁ M₂}
+-- definition graded_homotopy_elim' [unfold 8] := @graded_homotopy_of_deg.elim'
+-- definition graded_homotopy_elim [reducible] [unfold 8] [coercion] (h : f₁ ~[d] f₂) (i : I) :
+--   f₁ (refl i) ~ f₂ (refl i) :=
+-- graded_homotopy_elim' _ _
+
+-- definition graded_homotopy_elim_in [reducible] [unfold 8] (f : M₁ →gm M₂) (i : I) : M₁ ((deg f)⁻¹ i) →lm M₂ i :=
+-- f ↘ (to_right_inv (deg f) i)
+
+definition graded_homotopy_of_deg.mk [constructor] (h : Πi, f₁ (idpath (d i)) ~ f₂ (idpath (d i))) :
+  f₁ ~[d] f₂ :=
+begin
+  intro i j p, induction p, exact h i
+end
+
+-- definition graded_homotopy.mk_in [constructor] {M₁ M₂ : graded_module R I} (d : I ≃ I)
+--   (fn : Πi, M₁ (d⁻¹ i) →lm M₂ i) : M₁ →gm M₂ :=
+-- graded_hom.mk' d (λi j p, fn j ∘lm homomorphism_of_eq (ap M₁ (eq_inv_of_eq p)))
+-- definition is_gconstant (f : M₁ →gm M₂) : Type :=
+-- f↘ ~[deg f] gmd0
+
+definition compose_constant (f' : M₂ →gm M₃) (f : M₁ →gm M₂) : Type :=
+Π⦃i j k : I⦄ (p : deg f i = j) (q : deg f' j = k) (m : M₁ i), f' ↘ q (f ↘ p m) = 0
+
+definition compose_constant.mk (h : Πi m, f' (deg f i) (f i m) = 0) : compose_constant f' f :=
+by intros; induction p; induction q; exact h i m
+
+definition compose_constant.elim (h : compose_constant f' f) (i : I) (m : M₁ i) : f' (deg f i) (f i m) = 0 :=
+h idp idp m
+
+definition is_gconstant (f : M₁ →gm M₂) : Type :=
+Π⦃i j : I⦄ (p : deg f i = j) (m : M₁ i), f ↘ p m = 0
+
+definition is_gconstant.mk (h : Πi m, f i m = 0) : is_gconstant f :=
+by intros; induction p; exact h i m
+
+definition is_gconstant.elim (h : is_gconstant f) (i : I) (m : M₁ i) : f i m = 0 :=
+h idp m
+
 /- direct sum of graded R-modules -/
 
 variables {J : Set} (N : graded_module R J)
@@ -189,14 +280,59 @@ LeftModule_of_AddAbGroup (dirsum' N) (λr n, dirsum_smul r n)
   dirsum_mul_smul
   dirsum_one_smul
 
-/- homology of a graded module-homomorphism -/
+/- graded variants of left-module constructions -/
 
+definition graded_submodule [constructor] (S : Πi, submodule_rel (M i)) : graded_module R I :=
+λi, submodule (S i)
+
+definition graded_submodule_incl [constructor] (S : Πi, submodule_rel (M i)) :
+  graded_submodule S →gm M :=
+graded_hom.mk erfl (λi, submodule_incl (S i))
+
+definition graded_hom_lift [constructor] {S : Πi, submodule_rel (M₂ i)} (φ : M₁ →gm M₂)
+  (h : Π(i : I) (m : M₁ i), S (deg φ i) (φ i m)) : M₁ →gm graded_submodule S :=
+graded_hom.mk (deg φ) (λi, hom_lift (φ i) (h i))
+
+definition graded_image (f : M₁ →gm M₂) : graded_module R I :=
+λi, image_module (f ↘ (to_right_inv (deg f) i))
+
+definition graded_image_lift [constructor] (f : M₁ →gm M₂) : M₁ →gm graded_image f :=
+graded_hom.mk_in (deg f) (λi, image_lift (f ↘ (to_right_inv (deg f) i)))
+
+definition graded_image_elim [constructor] {f : M₁ →gm M₂} (g : M₁ →gm M₃)
+  (h : Π⦃i m⦄, f i m = 0 → g i m = 0) :
+  graded_image f →gm M₃ :=
+begin
+  apply graded_hom.mk_out_in (deg f) (deg g),
+  intro i,
+  apply image_elim (g ↘ (ap (deg g) (to_left_inv (deg f) i))),
+  intro m p,
+  refine graded_hom_eq_zero m (h _),
+  exact graded_hom_eq_zero m p
+end
+
+definition graded_quotient (S : Πi, submodule_rel (M i)) : graded_module R I :=
+λi, quotient_module (S i)
+
+definition graded_quotient_map [constructor] (S : Πi, submodule_rel (M i)) :
+  M →gm graded_quotient S :=
+graded_hom.mk erfl (λi, quotient_map (S i))
+
+definition graded_homology (g : M₂ →gm M₃) (f : M₁ →gm M₂) : graded_module R I :=
+λi, homology (g i) (f ↘ (to_right_inv (deg 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 _ _))
 
 
 /- exact couples -/
 
 definition is_exact_gmod (f : M₁ →gm M₂) (f' : M₂ →gm M₃) : Type :=
-Π{i j k} (p : deg f i = j) (q : deg f' j = k), is_exact_mod (↘f p) (↘f' q)
+Π⦃i j k⦄ (p : deg f i = j) (q : deg f' j = k), is_exact_mod (f ↘ p) (f' ↘ q)
+
+definition gmod_im_in_ker (h : is_exact_gmod f f') : compose_constant f' f :=
+λi j k p q, is_exact.im_in_ker (h p q)
 
 structure exact_couple (M₁ M₂ : graded_module R I) : Type :=
   (i : M₁ →gm M₁) (j : M₁ →gm M₂) (k : M₂ →gm M₁)
@@ -204,14 +340,62 @@ structure exact_couple (M₁ M₂ : graded_module R I) : Type :=
   (exact_jk : is_exact_gmod j k)
   (exact_ki : is_exact_gmod k i)
 
-  variables {i : M₁ →gm M₁} {j : M₁ →gm M₂} {k : M₂ →gm M₁}
+end left_module
+
+namespace left_module
+  namespace derived_couple
+  section
+  parameters {R : Ring} {I : Type} {D E : graded_module R I} {i : D →gm D} {j : D →gm E} {k : E →gm D}
             (exact_ij : is_exact_gmod i j)
             (exact_jk : is_exact_gmod j k)
             (exact_ki : is_exact_gmod k i)
 
-  namespace derived_couple
+  definition d : E →gm E := j ∘gm k
+  definition D' : graded_module R I := graded_image i
+  definition E' : graded_module R I := graded_homology d d
+  definition i' : D' →gm D' := graded_image_lift i ∘gm graded_submodule_incl _
+  include exact_jk exact_ki
 
-  definition d : M₂ →gm M₂ := j ∘gm k
+  theorem j_lemma1 ⦃x : I⦄ (m : D x) : d ((deg j) x) (j x m) = 0 :=
+  begin
+    rewrite [graded_hom_compose_fn,↑d,graded_hom_compose_fn],
+    refine ap (graded_hom_fn j (deg k (deg j x))) _ ⬝ !to_respect_zero,
+    exact compose_constant.elim (gmod_im_in_ker exact_jk) x m
+  end
+
+  theorem 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' _ :=
+  begin
+    have Π⦃x : I⦄ ⦃m : D (deg k x)⦄ (p : i (deg k x) m = 0), image (d x) (j (deg k x) m),
+    begin
+      intros,
+      note m_in_im_k := is_exact.ker_in_im (exact_ki idp _) _ p,
+      induction m_in_im_k with e q,
+      induction q,
+      apply image.mk e idp
+    end,
+    have Π⦃x : I⦄ ⦃m : D x⦄ (p : i x m = 0), image (d ← (deg j x)) (j x m),
+    begin
+      exact sorry
+    end,
+    intros,
+    rewrite [graded_hom_compose_fn],
+    exact quotient_map_eq_zero _ (this p)
+  end
+
+  definition j' : D' →gm E' :=
+  graded_image_elim (!graded_quotient_map ∘gm graded_hom_lift j j_lemma1) j_lemma2
+
+  definition k' : E' →gm D' :=
+  graded_homology_elim (graded_image_lift i ∘gm k)
+    abstract begin
+      apply compose_constant.mk, intro x m,
+      rewrite [graded_hom_compose_fn],
+      refine ap (graded_hom_fn (graded_image_lift i) (deg k (deg d x))) _ ⬝ !to_respect_zero,
+      exact compose_constant.elim (gmod_im_in_ker exact_jk) (deg k x) (k x m)
+    end end
+
+  end
 
   end derived_couple
 
diff --git a/algebra/left_module.hlean b/algebra/left_module.hlean
index d51514e..3531b86 100644
--- a/algebra/left_module.hlean
+++ b/algebra/left_module.hlean
@@ -141,8 +141,17 @@ section module_hom
 
   proposition respect_smul_add_smul (a b : R) (u v : M₁) : f (a • u + b • v) = a • f u + b • f v :=
   by rewrite [respect_add f, +respect_smul R f]
+
 end module_hom
 
+section hom_constant
+  variables {R : Type} {M₁ M₂ : Type}
+  variables [ring R] [has_scalar R M₁] [add_group M₁] [left_module R M₂]
+  proposition is_module_hom_constant : is_module_hom R (const M₁ (0 : M₂)) :=
+  (λm₁ m₂, !add_zero⁻¹, λr m, (smul_zero r)⁻¹ᵖ)
+
+end hom_constant
+
 structure LeftModule (R : Ring) :=
 (carrier : Type) (struct : left_module R carrier)
 
@@ -290,6 +299,9 @@ end
   abbreviation lmid [constructor] := homomorphism_id M
   infixr ` ∘lm `:75 := homomorphism_compose
 
+  definition lm_constant [constructor] (M₁ M₂ : LeftModule R) : M₁ →lm M₂ :=
+  homomorphism.mk (const M₁ 0) !is_module_hom_constant
+
   structure isomorphism (M₁ M₂ : LeftModule R) :=
     (to_hom : M₁ →lm M₂)
     (is_equiv_to_hom : is_equiv to_hom)
diff --git a/algebra/quotient_group.hlean b/algebra/quotient_group.hlean
index f1a8bbd..89cae13 100644
--- a/algebra/quotient_group.hlean
+++ b/algebra/quotient_group.hlean
@@ -159,7 +159,7 @@ namespace group
   end
 
   namespace quotient
-    notation `⟦`:max a `⟧`:0 := qg_map a _
+    notation `⟦`:max a `⟧`:0 := qg_map _ a
   end quotient
 
   open quotient
@@ -501,4 +501,48 @@ definition codomain_surjection_is_quotient_triangle {A B : AbGroup} (f : A →g
 
   end
 
-  end group
+end group
+
+namespace group
+
+  variables {G H K : Group} {R : normal_subgroup_rel G} {S : normal_subgroup_rel H}
+    {T : normal_subgroup_rel K}
+
+  definition quotient_ab_group_functor [constructor] {G H : AbGroup} {R : subgroup_rel G}
+    {S : subgroup_rel H} (φ : G →g H)
+    (h : Πg, R g → S (φ g)) : quotient_ab_group R →g quotient_ab_group S :=
+  quotient_group_functor φ h
+
+  theorem quotient_group_functor_compose (ψ : H →g K) (φ : G →g H)
+    (hψ : Πg, S g → T (ψ g)) (hφ : Πg, R g → S (φ g)) :
+    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.{u₁ v₁ u₂ v₂}
+    {G H : AbGroup} {R : subgroup_rel.{u₁ v₁} G} {S : subgroup_rel.{u₂ v₂} H}
+    (ψ φ : G →g H) (hψ : Πg, R g → S (ψ g)) (hφ : Πg, R g → S (φ g)) :
+    homomorphism_mul (quotient_ab_group_functor ψ hψ) (quotient_ab_group_functor φ hφ) ~
+    quotient_ab_group_functor (homomorphism_mul ψ φ)
+                        (λg hg, subgroup_respect_mul S (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, R g → S (φ g)) (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/subgroup.hlean b/algebra/subgroup.hlean
index 5c7f336..17349ae 100644
--- a/algebra/subgroup.hlean
+++ b/algebra/subgroup.hlean
@@ -127,7 +127,7 @@ namespace group
   abbreviation is_normal_subgroup   [unfold 2] := @normal_subgroup_rel.is_normal_subgroup
 
   section
-  variables {G G' : Group} (H : subgroup_rel G) (N : normal_subgroup_rel G) {g g' h h' k : G}
+  variables {G G' G₁ G₂ G₃ : Group} (H : subgroup_rel G) (N : normal_subgroup_rel G) {g g' h h' k : G}
             {A B : AbGroup}
 
   theorem is_normal_subgroup' (h : G) (r : N g) : N (h⁻¹ * g * h) :=
@@ -315,14 +315,14 @@ namespace group
     reflexivity
   end
 
-  definition iso_surjection_ab_image_incl {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 is_equiv_surjection_ab_image_incl f H
   end
 
-  definition hom_lift {G H : Group} (f : G →g H) (K : subgroup_rel H) (Hyp : Π (g : G), K (f g)) : G →g subgroup K :=
+  definition hom_lift [constructor] {G H : Group} (f : G →g H) (K : subgroup_rel H) (Hyp : Π (g : G), K (f g)) : G →g subgroup K :=
   begin
     fapply homomorphism.mk,
     intro g,
@@ -332,7 +332,7 @@ namespace group
     intro g h, apply subtype_eq, esimp, apply respect_mul
   end
 
-  definition image_lift {G H : Group} (f : G →g H) : G →g image f :=
+  definition image_lift [constructor] {G H : Group} (f : G →g H) : G →g image f :=
   begin
     fapply hom_lift f,
     intro g,
@@ -368,6 +368,24 @@ namespace group
     intro x,
     fapply image_incl_injective f x 1,
   end
+
+  definition image_elim_lemma {f₁ : G₁ →g G₂} {f₂ : G₁ →g G₃} (h : Π⦃g⦄, f₁ g = 1 → f₂ g = 1)
+    (g g' : G₁) (p : f₁ g = f₁ g') : f₂ g = f₂ g' :=
+  have f₁ (g * g'⁻¹) = 1, from !to_respect_mul ⬝ ap (mul _) !to_respect_inv ⬝
+    mul_inv_eq_of_eq_mul (p ⬝ !one_mul⁻¹),
+  have f₂ (g * g'⁻¹) = 1, from h this,
+  eq_of_mul_inv_eq_one (ap (mul _) !to_respect_inv⁻¹ ⬝ !to_respect_mul⁻¹ ⬝ this)
+
+  open image
+  definition image_elim {f₁ : G₁ →g G₂} (f₂ : G₁ →g G₃) (h : Π⦃g⦄, f₁ g = 1 → f₂ g = 1) :
+    image f₁ →g G₃ :=
+  homomorphism.mk (total_image.elim_set f₂ (image_elim_lemma h))
+  begin
+    refine total_image.rec _, intro g,
+    refine total_image.rec _, intro g',
+    exact to_respect_mul f₂ g g'
+  end
+
   end
 
   variables {G H K : Group} {R : subgroup_rel G} {S : subgroup_rel H} {T : subgroup_rel K}
@@ -446,3 +464,6 @@ namespace group
   end
 
 end group
+
+open group
+attribute image_subgroup [constructor]
diff --git a/algebra/submodule.hlean b/algebra/submodule.hlean
index 47dfc33..075ff3f 100644
--- a/algebra/submodule.hlean
+++ b/algebra/submodule.hlean
@@ -3,69 +3,13 @@ import .left_module .quotient_group
 
 open algebra eq group sigma is_trunc function trunc
 
-/- move to subgroup -/
-
-namespace group
-
-  variables {G H K : Group} {R : subgroup_rel G} {S : subgroup_rel H} {T : subgroup_rel K}
-
-  definition subgroup_functor_fun [unfold 7] (φ : G →g H) (h : Πg, R g → S (φ g)) (x : subgroup R) :
-    subgroup S :=
-  begin
-    induction x with g hg,
-    exact ⟨φ g, h g hg⟩
-  end
-
-  definition subgroup_functor [constructor] (φ : G →g H)
-    (h : Πg, R g → S (φ g)) : subgroup R →g subgroup S :=
-  begin
-    fapply homomorphism.mk,
-    { exact subgroup_functor_fun φ h },
-    { intro x₁ x₂, induction x₁ with g₁ hg₁, induction x₂ with g₂ hg₂,
-      exact sigma_eq !to_respect_mul !is_prop.elimo }
-  end
-
-  definition ab_subgroup_functor [constructor] {G H : AbGroup} {R : subgroup_rel G}
-    {S : subgroup_rel H} (φ : G →g H)
-    (h : Πg, R g → S (φ g)) : ab_subgroup R →g ab_subgroup S :=
-  subgroup_functor φ h
-
-  theorem subgroup_functor_compose (ψ : H →g K) (φ : G →g H)
-    (hψ : Πg, S g → T (ψ g)) (hφ : Πg, R g → S (φ g)) :
-    subgroup_functor ψ hψ ∘g subgroup_functor φ hφ ~
-    subgroup_functor (ψ ∘g φ) (λg, proof hψ (φ g) qed ∘ hφ g) :=
-  begin
-    intro g, induction g with g hg, reflexivity
-  end
-
-  definition subgroup_functor_gid : subgroup_functor (gid G) (λg, id) ~ gid (subgroup R) :=
-  begin
-    intro g, induction g with g hg, reflexivity
-  end
-
-  definition subgroup_functor_mul {G H : AbGroup} {R : subgroup_rel G} {S : subgroup_rel H}
-    (ψ φ : G →g H) (hψ : Πg, R g → S (ψ g)) (hφ : Πg, R g → S (φ g)) :
-    homomorphism_mul (ab_subgroup_functor ψ hψ) (ab_subgroup_functor φ hφ) ~
-    ab_subgroup_functor (homomorphism_mul ψ φ)
-                        (λg hg, subgroup_respect_mul S (hψ g hg) (hφ g hg)) :=
-  begin
-    intro g, induction g with g hg, reflexivity
-  end
-
-  definition subgroup_functor_homotopy {ψ φ : G →g H} (hψ : Πg, R g → S (ψ g))
-    (hφ : Πg, R g → S (φ g)) (p : φ ~ ψ) :
-    subgroup_functor φ hφ ~ subgroup_functor ψ hψ :=
-  begin
-    intro g, induction g with g hg,
-    exact subtype_eq (p g)
-  end
-
-
-end group open group
+-- move to subgroup
+attribute normal_subgroup_rel._trans_of_to_subgroup_rel [unfold 2]
+attribute normal_subgroup_rel.to_subgroup_rel [constructor]
 
 namespace left_module
 /- submodules -/
-variables {R : Ring} {M : LeftModule R} {m m₁ m₂ : M}
+variables {R : Ring} {M M₁ M₂ : LeftModule R} {m m₁ m₂ : M}
 
 structure submodule_rel (M : LeftModule R) : Type :=
   (S : M → Prop)
@@ -140,6 +84,13 @@ lm_homomorphism_of_group_homomorphism (incl_of_subgroup _)
     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 :=
+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 incl_smul (S : submodule_rel M) (r : R) (m : M) (h : S m) :
   r • ⟨m, h⟩ = ⟨_, contains_smul S r h⟩ :> submodule S :=
 by reflexivity
@@ -155,53 +106,6 @@ submodule_rel.mk (λm, S₁ (submodule_incl S₂ m))
 
 end left_module
 
-/- move to quotient_group -/
-
-namespace group
-
-  variables {G H K : Group} {R : normal_subgroup_rel G} {S : normal_subgroup_rel H}
-    {T : normal_subgroup_rel K}
-
-  definition quotient_ab_group_functor [constructor] {G H : AbGroup} {R : subgroup_rel G}
-    {S : subgroup_rel H} (φ : G →g H)
-    (h : Πg, R g → S (φ g)) : quotient_ab_group R →g quotient_ab_group S :=
-  quotient_group_functor φ h
-
-  theorem quotient_group_functor_compose (ψ : H →g K) (φ : G →g H)
-    (hψ : Πg, S g → T (ψ g)) (hφ : Πg, R g → S (φ g)) :
-    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
-
-set_option pp.universes true
-  definition quotient_group_functor_mul.{u₁ v₁ u₂ v₂}
-    {G H : AbGroup} {R : subgroup_rel.{u₁ v₁} G} {S : subgroup_rel.{u₂ v₂} H}
-    (ψ φ : G →g H) (hψ : Πg, R g → S (ψ g)) (hφ : Πg, R g → S (φ g)) :
-    homomorphism_mul (quotient_ab_group_functor ψ hψ) (quotient_ab_group_functor φ hφ) ~
-    quotient_ab_group_functor (homomorphism_mul ψ φ)
-                        (λg hg, subgroup_respect_mul S (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, R g → S (φ g)) (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 open group
-
 namespace left_module
 
 /- quotient modules -/
@@ -247,9 +151,22 @@ LeftModule_of_AddAbGroup (quotient_module' S) (quotient_module_smul S)
   quotient_module_mul_smul
   quotient_module_one_smul
 
-definition quotient_map (S : submodule_rel M) : M →lm quotient_module S :=
+definition quotient_map [constructor] (S : submodule_rel M) : 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
+
+definition quotient_elim [constructor] (φ : M →lm M₂) (H : Π⦃m⦄, S m → φ m = 0) :
+  quotient_module S →lm M₂ :=
+lm_homomorphism_of_group_homomorphism
+  (quotient_group_elim (group_homomorphism_of_lm_homomorphism φ) H)
+  begin
+    intro r m, esimp,
+    induction m using set_quotient.rec_prop with m,
+    exact to_respect_smul φ r m
+  end
+
 /- specific submodules -/
 definition has_scalar_image (φ : M₁ →lm M₂) ⦃m : M₂⦄ (r : R)
   (h : image φ m) : image φ (r • m) :=
@@ -259,26 +176,48 @@ begin
   refine to_respect_smul φ r m' ⬝ ap (λx, r • x) p,
 end
 
-definition image_rel (φ : M₁ →lm M₂) : submodule_rel M₂ :=
+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_module [constructor] (φ : M₁ →lm M₂) : LeftModule R := submodule (image_rel φ)
+
+-- unfortunately this is note definitionally equal:
+-- definition foo (φ : M₁ →lm M₂) :
+--   (image_module φ : AddAbGroup) = image (group_homomorphism_of_lm_homomorphism φ) :=
+-- by reflexivity
+
+variables {ψ : 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) _,
+  split,
+  { apply homomorphism.addstruct },
+  { intro r, refine @total_image.rec _ _ _ _ (λx, !is_trunc_eq) _, intro g,
+    apply to_respect_smul }
+end
+
 definition has_scalar_kernel (φ : M₁ →lm M₂) ⦃m : M₁⦄ (r : R)
   (p : φ m = 0) : φ (r • m) = 0 :=
 begin
   refine to_respect_smul φ r m ⬝ ap (λx, r • x) p ⬝ smul_zero r,
 end
 
-definition kernel_rel (φ : M₁ →lm M₂) : submodule_rel M₁ :=
+definition kernel_rel [constructor](φ : M₁ →lm M₂) : submodule_rel M₁ :=
 submodule_rel_of_subgroup_rel
   (kernel_subgroup (group_homomorphism_of_lm_homomorphism φ))
   (has_scalar_kernel φ)
 
+definition kernel_module [constructor] (φ : M₁ →lm M₂) : LeftModule R := submodule (kernel_rel φ)
+
+definition image_lift [constructor] (φ : M₁ →lm M₂) : M₁ →lm image_module φ :=
+hom_lift φ (λm, image.mk m idp)
+
 definition homology (ψ : M₂ →lm M₃) (φ : M₁ →lm M₂) : LeftModule R :=
 @quotient_module R (submodule (kernel_rel ψ)) (submodule_rel_of_submodule _ (image_rel φ))
 
-variables {ψ : M₂ →lm M₃} {φ : M₁ →lm M₂} (h : Πm, ψ (φ m) = 0)
 definition homology.mk (m : M₂) (h : ψ m = 0) : homology ψ φ :=
 quotient_map _ ⟨m, h⟩
 
@@ -294,6 +233,19 @@ definition homology_eq {m n : M₂} {hm : ψ m = 0} {hn : ψ n = 0} (h : image 
   homology.mk m hm = homology.mk n hn :> homology ψ φ :=
 eq_of_sub_eq_zero (homology_eq0 h)
 
+definition homology_elim [constructor] (θ : M₂ →lm M) (H : Πm, θ (φ m) = 0) :
+  homology ψ φ →lm M :=
+quotient_elim (θ ∘lm submodule_incl _)
+  begin
+    intro m x,
+    induction m with m h,
+    esimp at *,
+    induction x with v, induction v with m' p,
+    exact ap θ p⁻¹ ⬝ H m'
+  end
+
+-- remove:
+
 -- definition homology.rec (P : homology ψ φ → Type)
 --   [H : Πx, is_set (P x)] (h₀ : Π(m : M₂) (h : ψ m = 0), P (homology.mk m h))
 --   (h₁ : Π(m : M₂) (h : ψ m = 0) (k : image φ m), h₀ m h =[homology_eq0' k] h₀ 0 (to_respect_zero ψ))
@@ -302,10 +254,33 @@ eq_of_sub_eq_zero (homology_eq0 h)
 --   refine @set_quotient.rec _ _ _ H _ _,
 --   { intro v, induction v with m h, exact h₀ m h },
 --   { intro v v', induction v with m hm, induction v' with n hn,
---     esimp, intro h,
---     exact change_path _ _, }
+--     intro h,
+--     note x := h₁ (m - n) _ h,
+--     esimp,
+--     exact change_path _ _,
+-- }
 -- end
 
+  -- definition quotient.rec (P : quotient_group N → Type)
+  --   [H : Πx, is_set (P x)] (h₀ : Π(g : G), P (qg_map N g))
+  --   -- (h₀_mul : Π(g h : G), h₀ (g * h))
+  --   (h₁ : Π(g : G) (h : N g), h₀ g =[qg_map_eq_one g h] h₀ 1)
+  --   : Πx, P x :=
+  -- begin
+  --   refine @set_quotient.rec _ _ _ H _ _,
+  --   { intro g, exact h₀ g },
+  --   { intro g g' h,
+  --     note x := h₁ (g * g'⁻¹) h,
+  --     }
+  -- --   { intro v, induction  },
+  -- --   { intro v v', induction v with m hm, induction v' with n hn,
+  -- --     intro h,
+  -- --     note x := h₁ (m - n) _ h,
+  -- --     esimp,
+  -- --     exact change_path _ _,
+  -- -- }
+  -- end
+
 
 
 end left_module
diff --git a/move_to_lib.hlean b/move_to_lib.hlean
index 4f0b981..c2eec7b 100644
--- a/move_to_lib.hlean
+++ b/move_to_lib.hlean
@@ -1,10 +1,12 @@
 -- definitions, theorems and attributes which should be moved to files in the HoTT library
 
-import homotopy.sphere2 homotopy.cofiber homotopy.wedge
+import homotopy.sphere2 homotopy.cofiber homotopy.wedge hit.prop_trunc
 
 open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc_index pi group
      is_trunc function sphere unit sum prod bool
 
+attribute is_prop.elim_set [unfold 6]
+
 definition add_comm_right {A : Type} [add_comm_semigroup A] (n m k : A) : n + m + k = n + k + m :=
 !add.assoc ⬝ ap (add n) !add.comm ⬝ !add.assoc⁻¹
 
@@ -1106,6 +1108,29 @@ begin
   exact h
 end
 
+definition total_image {A B : Type} (f : A → B) : Type := sigma (image f)
+local attribute is_prop.elim_set [recursor 6]
+definition total_image.elim_set [unfold 8]
+  {A B : Type} {f : A → B} {C : Type} [is_set C]
+  (g : A → C) (h : Πa a', f a = f a' → g a = g a') (x : total_image f) : C :=
+begin
+  induction x with b v,
+  induction v using is_prop.elim_set with x x x',
+  { induction x with a p, exact g a },
+  { induction x with a p, induction x' with a' p', induction p', exact h _ _ p }
+end
+
+definition total_image.rec [unfold 7]
+  {A B : Type} {f : A → B} {C : total_image f → Type} [H : Πx, is_prop (C x)]
+  (g : Πa, C ⟨f a, image.mk a idp⟩)
+  (x : total_image f) : C x :=
+begin
+  induction x with b v,
+  refine @image.rec _ _ _ _ _ (λv, H ⟨b, v⟩) _ v,
+  intro a p,
+  induction p, exact g a
+end
+
 definition image.equiv_exists {A B : Type} {f : A → B} {b : B} : image f b ≃ ∃ a, f a = b :=
 trunc_equiv_trunc _ (fiber.sigma_char _ _)