diff --git a/algebra/graded.hlean b/algebra/graded.hlean
index 40df902..e7a5053 100644
--- a/algebra/graded.hlean
+++ b/algebra/graded.hlean
@@ -4,13 +4,14 @@
 
 import .left_module .direct_sum .submodule --..heq
 
-open is_trunc algebra eq left_module pointed function equiv is_equiv prod group sigma nat
-
+open is_trunc algebra eq left_module pointed function equiv is_equiv prod group sigma sigma.ops nat
+  trunc_index
 namespace left_module
 
 definition graded [reducible] (str : Type) (I : Type) : Type := I → str
 definition graded_module [reducible] (R : Ring) : Type → Type := graded (LeftModule R)
 
+-- TODO: We can (probably) make I a type everywhere
 variables {R : Ring} {I : Set} {M M₁ M₂ M₃ : graded_module R I}
 
 /-
@@ -58,7 +59,37 @@ f ↘ idp
 definition graded_hom_fn_out [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_out -- todo: change notation
+infix ` ← `:max := graded_hom_fn_out -- todo: change notation
+
+-- definition graded_hom_fn_out_rec (f : M₁ →gm M₂)
+--   (P : Π{i j} (p : deg f i = j) (m : M₁ i) (n : M₂ j), Type)
+--   (H : Πi m, P (right_inv (deg f) i) m (f ← i m)) {i j : I}
+--   (p : deg f i = j) (m : M₁ i) (n : M₂ j) : P p m (f ↘ p m) :=
+-- begin
+--   revert i j p m n, refine equiv_rect (deg f)⁻¹ᵉ _ _, intro i,
+--   refine eq.rec_to (right_inv (deg f) i) _,
+--   intro m n, exact H i m
+-- end
+
+-- definition graded_hom_fn_rec (f : M₁ →gm M₂)
+--   {P : Π{i j} (p : deg f i = j) (m : M₁ i) (n : M₂ j), Type}
+--   (H : Πi m, P idp m (f i m)) ⦃i j : I⦄
+--   (p : deg f i = j) (m : M₁ i) : P p m (f ↘ p m) :=
+-- begin
+--   induction p, apply H
+-- end
+
+-- definition graded_hom_fn_out_rec (f : M₁ →gm M₂)
+--   {P : Π{i j} (p : deg f i = j) (m : M₁ i) (n : M₂ j), Type}
+--   (H : Πi m, P idp m (f i m)) ⦃i : I⦄ (m : M₁ ((deg f)⁻¹ᵉ i)) :
+--   P (right_inv (deg f) i) m (f ← i m) :=
+-- graded_hom_fn_rec f H (right_inv (deg f) i) m
+
+-- definition graded_hom_fn_out_rec_simple (f : M₁ →gm M₂)
+--   {P : Π{j} (n : M₂ j), Type}
+--   (H : Πi m, P (f i m)) ⦃i : I⦄ (m : M₁ ((deg f)⁻¹ᵉ i)) :
+--   P (f ← i m) :=
+-- graded_hom_fn_out_rec f H m
 
 definition graded_hom.mk [constructor] (d : I ≃ I)
   (fn : Πi, M₁ i →lm M₂ (d i)) : M₁ →gm M₂ :=
@@ -85,21 +116,30 @@ definition graded_hom_mk_refl (d : I ≃ I)
   (fn : Πi, M₁ i →lm M₂ (d i)) {i : I} (m : M₁ i) : graded_hom.mk d fn i m = fn i m :=
 by reflexivity
 
-lemma graded_hom_mk_out'_left_inv (d : I ≃ I)
+lemma graded_hom_mk_out'_destruct (d : I ≃ I)
   (fn : Πi, M₁ (d i) →lm M₂ i) {i : I} (m : M₁ (d i)) :
   graded_hom.mk_out' d fn ↘ (left_inv d i) m = fn i m :=
 begin
   unfold [graded_hom.mk_out'],
   apply ap (λx, fn i (cast x m)),
   refine !ap_compose⁻¹ ⬝ ap02 _ _,
-  apply is_set.elim --we can also prove this in arbitrary types
+  apply is_set.elim --TODO: we can also prove this if I is not a set
 end
 
-lemma graded_hom_mk_out_right_inv (d : I ≃ I)
+lemma graded_hom_mk_out_destruct (d : I ≃ I)
   (fn : Πi, M₁ (d⁻¹ i) →lm M₂ i) {i : I} (m : M₁ (d⁻¹ i)) :
   graded_hom.mk_out d fn ↘ (right_inv d i) m = fn i m :=
 begin
-  rexact graded_hom_mk_out'_left_inv d⁻¹ᵉ fn m
+  rexact graded_hom_mk_out'_destruct d⁻¹ᵉ fn m
+end
+
+lemma graded_hom_mk_out_in_destruct (d₁ : I ≃ I) (d₂ : I ≃ I)
+  (fn : Πi, M₁ (d₁ i) →lm M₂ (d₂ i)) {i : I} (m : M₁ (d₁ i)) :
+  graded_hom.mk_out_in d₁ d₂ fn ↘ (ap d₂ (left_inv d₁ i)) m = fn i m :=
+begin
+  unfold [graded_hom.mk_out_in],
+  rewrite [adj d₁, -ap_inv, - +ap_compose, ],
+  refine cast_fn_cast_square fn _ _ !con.left_inv m
 end
 
 definition graded_hom_eq_zero {f : M₁ →gm M₂} {i j k : I} {q : deg f i = j} {p : deg f i = k}
@@ -107,16 +147,48 @@ definition graded_hom_eq_zero {f : M₁ →gm M₂} {i j k : I} {q : deg f i = j
 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))
 
+definition graded_hom_change_image {f : M₁ →gm M₂} {i j k : I} {m : M₂ k} (p : deg f i = k)
+  (q : deg f j = k) (h : image (f ↘ p) m) : image (f ↘ q) m :=
+begin
+  have Σ(r : i = j), ap (deg f) r = p ⬝ q⁻¹,
+  from ⟨eq_of_fn_eq_fn (deg f) (p ⬝ q⁻¹), !ap_eq_of_fn_eq_fn'⟩,
+  induction this with r s, induction r, induction q, esimp at s, induction s, exact h
+end
+
+definition graded_hom_codom_rec {f : M₁ →gm M₂} {j : I} {P : Π⦃i⦄, deg f i = j → Type}
+  {i i' : I} (p : deg f i = j) (h : P p) (q : deg f i' = j) : P q :=
+begin
+  have Σ(r : i = i'), ap (deg f) r = p ⬝ q⁻¹,
+  from ⟨eq_of_fn_eq_fn (deg f) (p ⬝ q⁻¹), !ap_eq_of_fn_eq_fn'⟩,
+  induction this with r s, induction r, induction q, esimp at s, induction s, exact h
+end
+
 variables {f' : M₂ →gm M₃} {f g h : M₁ →gm M₂}
 
 definition graded_hom_compose [constructor] (f' : M₂ →gm M₃) (f : M₁ →gm M₂) : M₁ →gm M₃ :=
-graded_hom.mk (deg f ⬝e deg f') (λi, f' (deg f i) ∘lm f i)
+graded_hom.mk' (deg f ⬝e deg f') (λi j p, f' ↘ p ∘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
+by reflexivity
+
+definition graded_hom_compose_fn_ext (f' : M₂ →gm M₃) (f : M₁ →gm M₂) ⦃i j k : I⦄
+  (p : deg f i = j) (q : deg f' j = k) (r : (deg f ⬝e deg f') i = k) (s : ap (deg f') p ⬝ q = r)
+  (m : M₁ i) : ((f' ∘gm f) ↘ r) m = (f' ↘ q) (f ↘ p m) :=
+by induction s; induction q; induction p; reflexivity
+
+definition graded_hom_compose_fn_out (f' : M₂ →gm M₃) (f : M₁ →gm M₂) (i : I)
+  (m : M₁ ((deg f ⬝e deg f')⁻¹ᵉ i)) : (f' ∘gm f) ← i m = f' ← i (f ← ((deg f')⁻¹ᵉ i) m) :=
+graded_hom_compose_fn_ext f' f _ _ _ idp m
+
+-- the following composition might be useful if you want tight control over the paths to which f and f' are applied
+definition graded_hom_compose_ext [constructor] (f' : M₂ →gm M₃) (f : M₁ →gm M₂)
+  (d : Π⦃i j⦄ (p : (deg f ⬝e deg f') i = j), I)
+  (pf  : Π⦃i j⦄ (p : (deg f ⬝e deg f') i = j), deg f i = d p)
+  (pf' : Π⦃i j⦄ (p : (deg f ⬝e deg f') i = j), deg f' (d p) = j) : M₁ →gm M₃ :=
+graded_hom.mk' (deg f ⬝e deg f') (λi j p, (f' ↘ (pf' p)) ∘lm (f ↘ (pf p)))
 
 variable (M)
 definition graded_hom_id [constructor] [refl] : M →gm M :=
@@ -245,27 +317,27 @@ end
 --   graded_hom.mk_out_in d₁⁻¹ᵉ d₂ _ :=
 -- _
 
-definition graded_hom_out_in_compose_out {d₁ d₂ d₃ : I ≃ I} (f₂ : Πi, M₂ (d₂ i) →lm M₃ (d₃ i))
-  (f₁ : Πi, M₁ (d₁⁻¹ i) →lm M₂ i) : graded_hom.mk_out_in d₂ d₃ f₂ ∘gm graded_hom.mk_out d₁ f₁ ~gm
-  graded_hom.mk_out_in (d₂ ⬝e d₁⁻¹ᵉ) d₃ (λi, f₂ i ∘lm (f₁ (d₂ i))) :=
-begin
-  apply graded_homotopy.mk, intro i m, exact sorry
-end
+-- definition graded_hom_out_in_compose_out {d₁ d₂ d₃ : I ≃ I} (f₂ : Πi, M₂ (d₂ i) →lm M₃ (d₃ i))
+--   (f₁ : Πi, M₁ (d₁⁻¹ i) →lm M₂ i) : graded_hom.mk_out_in d₂ d₃ f₂ ∘gm graded_hom.mk_out d₁ f₁ ~gm
+--   graded_hom.mk_out_in (d₂ ⬝e d₁⁻¹ᵉ) d₃ (λi, f₂ i ∘lm (f₁ (d₂ i))) :=
+-- begin
+--   apply graded_homotopy.mk, intro i m, exact sorry
+-- end
 
-definition graded_hom_out_in_rfl {d₁ d₂ : I ≃ I} (f : Πi, M₁ i →lm M₂ (d₂ i))
-  (p : Πi, d₁ i = i) :
-  graded_hom.mk_out_in d₁ d₂ (λi, sorry) ~gm graded_hom.mk d₂ f :=
-begin
-  apply graded_homotopy.mk, intro i m, exact sorry
-end
+-- definition graded_hom_out_in_rfl {d₁ d₂ : I ≃ I} (f : Πi, M₁ i →lm M₂ (d₂ i))
+--   (p : Πi, d₁ i = i) :
+--   graded_hom.mk_out_in d₁ d₂ (λi, sorry) ~gm graded_hom.mk d₂ f :=
+-- begin
+--   apply graded_homotopy.mk, intro i m, exact sorry
+-- end
 
-definition graded_homotopy.trans (h₁ : f ~gm g) (h₂ : g ~gm h) : f ~gm h :=
-begin
-  exact sorry
-end
+-- definition graded_homotopy.trans (h₁ : f ~gm g) (h₂ : g ~gm h) : f ~gm h :=
+-- begin
+--   exact sorry
+-- end
 
 -- postfix `⁻¹ᵍᵐ`:(max + 1) := graded_iso.symm
-infixl ` ⬝gm `:75 := graded_homotopy.trans
+--infixl ` ⬝gm `:75 := graded_homotopy.trans
 -- infixl ` ⬝gmp `:75 := graded_iso.trans_eq
 -- infixl ` ⬝pgm `:75 := graded_iso.eq_trans
 
@@ -361,11 +433,52 @@ definition graded_hom_lift [constructor] {S : Πi, submodule_rel (M₂ i)}
   (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_submodule_functor [constructor] {S : Πi, submodule_rel (M₁ i)}
+  {T : Πi, submodule_rel (M₂ 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))
+
 definition graded_image (f : M₁ →gm M₂) : graded_module R I :=
 λi, image_module (f ← i)
 
+lemma graded_image_lift_lemma (f : M₁ →gm M₂) {i j: I} (p : deg f i = j) (m : M₁ i) :
+  image (f ← j) (f ↘ p m) :=
+graded_hom_change_image p (right_inv (deg f) j) (image.mk m idp)
+
 definition graded_image_lift [constructor] (f : M₁ →gm M₂) : M₁ →gm graded_image f :=
-graded_hom.mk_out (deg f) (λi, image_lift (f ← i))
+graded_hom.mk' (deg f) (λi j p, hom_lift (f ↘ p) (graded_image_lift_lemma f p))
+
+definition graded_image_lift_destruct (f : M₁ →gm M₂) {i : I}
+  (m : M₁ ((deg f)⁻¹ᵉ i)) : graded_image_lift f ← i m = image_lift (f ← i) m :=
+subtype_eq idp
+
+definition graded_image.rec {f : M₁ →gm M₂} {i : I} {P : graded_image f (deg f i) → Type}
+  [h : Πx, is_prop (P x)] (H : Πm, P (graded_image_lift f i m)) : Πm, P m :=
+begin
+  assert H₂ : Πi' (p : deg f i' = deg f i) (m : M₁ i'),
+    P ⟨f ↘ p m, graded_hom_change_image p _ (image.mk m idp)⟩,
+  { refine eq.rec_equiv_symm (deg f) _, intro m,
+    refine transport P _ (H m), apply subtype_eq, reflexivity },
+  refine @total_image.rec _ _ _ _ h _, intro m,
+  refine transport P _ (H₂ _ (right_inv (deg f) (deg f i)) m),
+  apply subtype_eq, reflexivity
+end
+
+definition image_graded_image_lift {f : M₁ →gm M₂} {i j : I} (p : deg f i = j)
+  (m : graded_image f j)
+  (h : image (f ↘ p) m.1) : image (graded_image_lift f ↘ p) m :=
+begin
+  induction p,
+  revert m h, refine total_image.rec _, intro m h,
+  induction h with n q, refine image.mk n (subtype_eq q)
+end
+
+lemma is_surjective_graded_image_lift ⦃x y⦄ (f : M₁ →gm M₂)
+  (p : deg f x = y) : is_surjective (graded_image_lift f ↘ p) :=
+begin
+  intro m, apply image_graded_image_lift, exact graded_hom_change_image (right_inv (deg f) y) _ m.2
+end
 
 definition graded_image_elim [constructor] {f : M₁ →gm M₂} (g : M₁ →gm M₃)
   (h : Π⦃i m⦄, f i m = 0 → g i m = 0) :
@@ -374,85 +487,103 @@ 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
+  exact abstract begin
+    intro m p,
+    refine graded_hom_eq_zero m (h _),
+    exact graded_hom_eq_zero m p end end
 end
 
-definition is_surjective_graded_image_lift ⦃x y⦄ (f : M₁ →gm M₂)
-  (p : deg f x = y) : is_surjective (graded_image_lift f ↘ p) :=
+lemma graded_image_elim_destruct {f : M₁ →gm M₂} {g : M₁ →gm M₃}
+  (h : Π⦃i m⦄, f i m = 0 → g i m = 0) {i j k : I}
+  (p' : deg f i = j) (p : deg g ((deg f)⁻¹ᵉ j) = k)
+  (q : deg g i = k) (r : ap (deg g) (to_left_inv (deg f) i) ⬝ q = ap ((deg f)⁻¹ᵉ ⬝e deg g) p' ⬝ p)
+  (m : M₁ i) : graded_image_elim g h ↘ p (graded_image_lift f ↘ p' m) =
+  g ↘ q m :=
 begin
-  exact sorry
+  revert i j p' k p q r m,
+  refine equiv_rect (deg f ⬝e (deg f)⁻¹ᵉ) _ _,
+  intro i, refine eq.rec_grading _ (deg f) (right_inv (deg f) (deg f i)) _,
+  intro k p q r m,
+  assert r' : q = p,
+  { refine cancel_left _ (r ⬝ whisker_right _ _), refine !ap_compose ⬝ ap02 (deg g) _,
+    exact !adj_inv⁻¹ },
+  induction r', clear r,
+  revert k q m, refine eq.rec_to (ap (deg g) (to_left_inv (deg f) i)) _, intro m,
+  refine graded_hom_mk_out_in_destruct (deg f) (deg g) _ (graded_image_lift f ← (deg f i) m) ⬝ _,
+  refine ap (image_elim _ _) !graded_image_lift_destruct ⬝ _, reflexivity
 end
 
-definition graded_image' (f : M₁ →gm M₂) : graded_module R I :=
-λi, image_module (f i)
+/- alternative (easier) definition of graded_image with "wrong" grading -/
 
-definition graded_image'_lift [constructor] (f : M₁ →gm M₂) : M₁ →gm graded_image' f :=
-graded_hom.mk erfl (λi, image_lift (f i))
+-- definition graded_image' (f : M₁ →gm M₂) : graded_module R I :=
+-- λi, image_module (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 (deg g),
-  intro i,
-  apply image_elim (g i),
-  intro m p, exact h p
-end
+-- definition graded_image'_lift [constructor] (f : M₁ →gm M₂) : M₁ →gm graded_image' f :=
+-- graded_hom.mk erfl (λi, image_lift (f i))
 
-theorem graded_image'_elim_compute {f : M₁ →gm M₂} {g : M₁ →gm M₃}
-  (h : Π⦃i m⦄, f i m = 0 → g i m = 0) :
-  graded_image'_elim g h ∘gm graded_image'_lift f ~gm g :=
-begin
-  apply graded_homotopy.mk,
-  intro i m, exact sorry --reflexivity
-end
+-- 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 (deg g),
+--   intro i,
+--   apply image_elim (g i),
+--   intro m p, exact h p
+-- end
 
-theorem graded_image_elim_compute {f : M₁ →gm M₂} {g : M₁ →gm M₃}
-  (h : Π⦃i m⦄, f i m = 0 → g i m = 0) :
-  graded_image_elim g h ∘gm graded_image_lift f ~gm g :=
-begin
-  refine _ ⬝gm graded_image'_elim_compute h,
-  esimp, exact sorry
-  -- refine graded_hom_out_in_compose_out _ _ ⬝gm _, exact sorry
-  -- -- apply graded_homotopy.mk,
-  -- -- intro i m,
-end
-variables {α β : I ≃ I}
-definition gen_image (f : M₁ →gm M₂) (p : Πi, deg f (α i) = β i) : graded_module R I :=
-λi, image_module (f ↘ (p i))
+-- theorem graded_image'_elim_compute {f : M₁ →gm M₂} {g : M₁ →gm M₃}
+--   (h : Π⦃i m⦄, f i m = 0 → g i m = 0) :
+--   graded_image'_elim g h ∘gm graded_image'_lift f ~gm g :=
+-- begin
+--   apply graded_homotopy.mk,
+--   intro i m, exact sorry --reflexivity
+-- end
 
-definition gen_image_lift [constructor] (f : M₁ →gm M₂) (p : Πi, deg f (α i) = β i) : M₁ →gm gen_image f p :=
-graded_hom.mk_out α⁻¹ᵉ (λi, image_lift (f ↘ (p i)))
+-- theorem graded_image_elim_compute {f : M₁ →gm M₂} {g : M₁ →gm M₃}
+--   (h : Π⦃i m⦄, f i m = 0 → g i m = 0) :
+--   graded_image_elim g h ∘gm graded_image_lift f ~gm g :=
+-- begin
+--   refine _ ⬝gm graded_image'_elim_compute h,
+--   esimp, exact sorry
+--   -- refine graded_hom_out_in_compose_out _ _ ⬝gm _, exact sorry
+--   -- -- apply graded_homotopy.mk,
+--   -- -- intro i m,
+-- end
 
-definition gen_image_elim [constructor] {f : M₁ →gm M₂} (p : Πi, deg f (α i) = β i) (g : M₁ →gm M₃)
-  (h : Π⦃i m⦄, f i m = 0 → g i m = 0) :
-  gen_image f p →gm M₃ :=
-begin
-  apply graded_hom.mk_out_in α⁻¹ᵉ (deg g),
-  intro i,
-  apply image_elim (g ↘ (ap (deg g) (to_right_inv α i))),
-  intro m p,
-  refine graded_hom_eq_zero m (h _),
-  exact graded_hom_eq_zero m p
-end
+-- variables {α β : I ≃ I}
+-- definition gen_image (f : M₁ →gm M₂) (p : Πi, deg f (α i) = β i) : graded_module R I :=
+-- λi, image_module (f ↘ (p i))
 
-theorem gen_image_elim_compute {f : M₁ →gm M₂} {p : deg f ∘ α ~ β} {g : M₁ →gm M₃}
-  (h : Π⦃i m⦄, f i m = 0 → g i m = 0) :
-  gen_image_elim p g h ∘gm gen_image_lift f p ~gm g :=
-begin
-  -- induction β with β βe, esimp at *, induction p using homotopy.rec_on_idp,
-  assert q : β ⬝e (deg f)⁻¹ᵉ = α,
-  { apply equiv_eq, intro i, apply inv_eq_of_eq, exact (p i)⁻¹ },
-  induction q,
-  -- unfold [gen_image_elim, gen_image_lift],
+-- definition gen_image_lift [constructor] (f : M₁ →gm M₂) (p : Πi, deg f (α i) = β i) : M₁ →gm gen_image f p :=
+-- graded_hom.mk_out α⁻¹ᵉ (λi, image_lift (f ↘ (p i)))
 
-  -- induction (is_prop.elim (λi, to_right_inv (deg f) (β i)) p),
-  -- apply graded_homotopy.mk,
-  -- intro i m, reflexivity
-  exact sorry
-end
+-- definition gen_image_elim [constructor] {f : M₁ →gm M₂} (p : Πi, deg f (α i) = β i) (g : M₁ →gm M₃)
+--   (h : Π⦃i m⦄, f i m = 0 → g i m = 0) :
+--   gen_image f p →gm M₃ :=
+-- begin
+--   apply graded_hom.mk_out_in α⁻¹ᵉ (deg g),
+--   intro i,
+--   apply image_elim (g ↘ (ap (deg g) (to_right_inv α i))),
+--   intro m p,
+--   refine graded_hom_eq_zero m (h _),
+--   exact graded_hom_eq_zero m p
+-- end
+
+-- theorem gen_image_elim_compute {f : M₁ →gm M₂} {p : deg f ∘ α ~ β} {g : M₁ →gm M₃}
+--   (h : Π⦃i m⦄, f i m = 0 → g i m = 0) :
+--   gen_image_elim p g h ∘gm gen_image_lift f p ~gm g :=
+-- begin
+--   -- induction β with β βe, esimp at *, induction p using homotopy.rec_on_idp,
+--   assert q : β ⬝e (deg f)⁻¹ᵉ = α,
+--   { apply equiv_eq, intro i, apply inv_eq_of_eq, exact (p i)⁻¹ },
+--   induction q,
+--   -- unfold [gen_image_elim, gen_image_lift],
+
+--   -- induction (is_prop.elim (λi, to_right_inv (deg f) (β i)) p),
+--   -- apply graded_homotopy.mk,
+--   -- intro i m, reflexivity
+--   exact sorry
+-- end
 
 definition graded_kernel (f : M₁ →gm M₂) : graded_module R I :=
 λi, kernel_module (f i)
@@ -464,8 +595,21 @@ 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_quotient_elim [constructor] {S : Πi, submodule_rel (M 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 :=
-λi, homology (g i) (f ← i)
+graded_quotient (λi, submodule_rel_submodule (kernel_rel (g i)) (image_rel (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
+
+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 :=
+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 :=
@@ -475,6 +619,14 @@ definition graded_homology_elim {g : M₂ →gm M₃} {f : M₁ →gm M₂} (h :
   (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)
+end
+
 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)
 
@@ -486,11 +638,9 @@ begin intro i j k p q; induction p; induction q; split, apply h₁, apply h₂ e
 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)
 
--- definition is_exact_gmod_mk_mk_out' {d₁ d₂ : I ≃ I} (fn₁ : Πi, M₁ i →lm M₂ (d₁ i))
---   (fn₂ : Πi, M₂ (d₂ i) →lm M₃ i) (H : Πi, is_exact_mod (fn₁ i) _) : is_exact_gmod (graded_hom.mk d₁ fn₁) (graded_hom.mk_out' d₂ fn₂) :=
--- begin
-
--- end
+definition gmod_ker_in_im (h : is_exact_gmod f f') ⦃i : I⦄ (m : M₂ i) (p : f' i m = 0) :
+  image (f ← i) m :=
+is_exact.ker_in_im (h (right_inv (deg f) i) idp) m p
 
 
 end left_module
diff --git a/algebra/left_module.hlean b/algebra/left_module.hlean
index 819ded7..29727f8 100644
--- a/algebra/left_module.hlean
+++ b/algebra/left_module.hlean
@@ -234,6 +234,9 @@ section
     definition to_respect_smul (a : R) (x : M₁) : φ (a • x) = a • (φ x) :=
     respect_smul R φ a x
 
+    definition to_respect_sub (x y : M₁) : φ (x - y) = φ x - φ y :=
+    respect_sub φ x y
+
     definition is_embedding_of_homomorphism /- φ -/ (H : Π{x}, φ x = 0 → x = 0) : is_embedding φ :=
     is_embedding_of_is_add_hom φ @H
 
@@ -391,6 +394,10 @@ end
   definition is_exact_mod (f : M₁ →lm M₂) (f' : M₂ →lm M₃) : Type :=
   @is_exact M₁ M₂ M₃ (homomorphism_fn f) (homomorphism_fn f')
 
+  definition is_exact_mod.mk {f : M₁ →lm M₂} {f' : M₂ →lm M₃}
+    (h₁ : Πm, f' (f m) = 0) (h₂ : Πm, f' m = 0 → image f m) : is_exact_mod f f' :=
+  is_exact.mk h₁ h₂
+
   structure short_exact_mod (A B C : LeftModule R) :=
     (f : A →lm B)
     (g : B →lm C)
diff --git a/algebra/module_exact_couple.hlean b/algebra/module_exact_couple.hlean
index 257b57e..c595e6a 100644
--- a/algebra/module_exact_couple.hlean
+++ b/algebra/module_exact_couple.hlean
@@ -1,10 +1,13 @@
-/- Exact couples of graded (left-) R-modules. -/
+/- Exact couples of graded (left-) R-modules. This file includes:
+  - Constructing exact couples from sequences of maps
+  - Deriving an exact couple
+  - The convergence theorem for exact couples -/
 
 -- Author: Floris van Doorn
 
 import .graded ..homotopy.spectrum .product_group
 
-open algebra is_trunc left_module is_equiv equiv eq function nat
+open algebra is_trunc left_module is_equiv equiv eq function nat sigma sigma.ops set_quotient
 
 /- exact couples -/
 
@@ -17,9 +20,10 @@ namespace left_module
     (jk : is_exact_gmod j k)
     (ki : is_exact_gmod k i)
 
+  open exact_couple
+
   namespace derived_couple
   section
-  open exact_couple
 
   parameters {R : Ring} {I : Set} (X : exact_couple R I)
   local abbreviation D := D X
@@ -42,7 +46,7 @@ namespace left_module
   !is_contr_image_module
 
   definition i' : D' →gm D' :=
-  graded_image_lift i ∘gm graded_submodule_incl _
+  graded_image_lift i ∘gm graded_submodule_incl (λx, image_rel (i ← x))
   -- degree i + 0
 
   lemma is_surjective_i' {x y : I} (p : deg i' x = y)
@@ -93,70 +97,126 @@ namespace left_module
   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) : image (i ← (deg k x)) (k x m) :=
-  begin
-    exact sorry
-  end
+  -- mk_out_in (deg f) (deg g)
 
-  lemma k_lemma2 : compose_constant (graded_hom_lift k k_lemma1 : E →gm D') d :=
+  lemma k_lemma1 ⦃x : I⦄ (m : E x) (p : d x m = 0) : image (i ← (deg k x)) (k x m) :=
+  gmod_ker_in_im (exact_couple.ij X) (k x m) p
+
+  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) :
+    k₂ x ⟨m, h₁⟩ = 0 :=
   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 jk) (deg k x) (k x m)
-    exact sorry
+    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'),
+      k ↘ r (j ↘ q (k ↘ p n)) = 0,
+    { intros, exact gmod_im_in_ker (exact_couple.jk X) q r (k ↘ p n) },
+    induction h₂ with n p,
+    assert H₂ : k x m = 0,
+    { rewrite [-p], refine ap (k x) (graded_hom_compose_fn_out j k x n) ⬝ _, apply H₁ },
+    exact subtype_eq H₂
   end
 
   definition k' : E' →gm D' :=
-  graded_homology_elim (graded_hom_lift k k_lemma1) k_lemma2
+  graded_quotient_elim (graded_submodule_functor k k_lemma1)
+                       (by intro x m h; exact k_lemma2 m.1 m.2 h)
+
+  definition i'_eq ⦃x : I⦄ (m : D x) (h : image (i ← x) m) : (i' x ⟨m, h⟩).1 = i x m :=
+  by reflexivity
+
+  definition k'_eq ⦃x : I⦄ (m : E x) (h : d x m = 0) : (k' x (class_of ⟨m, h⟩)).1 = k x m :=
+  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) :=
+  begin
+    refine graded_image_elim_destruct _ _ _ idp _ m,
+    apply is_set.elim,
+  end
 
   definition deg_i' : deg i' ~ deg i := by reflexivity
   definition deg_j' : deg j' ~ deg j ∘ (deg i)⁻¹ := by reflexivity
   definition deg_k' : deg k' ~ deg k := by reflexivity
 
+  open group
   lemma i'j' : is_exact_gmod i' j' :=
   begin
-    apply is_exact_gmod.mk,
-    { intro x, refine total_image.rec _, intro m, exact sorry
-      -- exact calc
-      --   j' (deg i' x) (i' x ⟨(i ← x) m, image.mk m idp⟩)
-      --       = j' (deg i' x) (graded_image_lift i x ((i ← x) m)) : idp
-      --   ... = graded_homology_intro d d (deg j ((deg i)⁻¹ᵉ (deg i x)))
-      --           (graded_hom_lift j j_lemma1 ((deg i)⁻¹ᵉ (deg i x))
-      --           (i ↘ (!to_right_inv ⬝ !to_left_inv⁻¹) m)) : _
-      --   ... = graded_homology_intro d d (deg j ((deg i)⁻¹ᵉ (deg i x)))
-      --           (graded_hom_lift j j_lemma1 ((deg i)⁻¹ᵉ (deg i x))
-      --           (i ↘ (!to_right_inv ⬝ !to_left_inv⁻¹) m)) : _
-      --   ... = 0 : _
-      },
-    { exact sorry }
+    intro x, refine equiv_rect (deg i) _ _,
+    intros y z p q, revert z q x p,
+    refine eq.rec_grading (deg i ⬝e deg j') (deg j) (ap (deg j) (left_inv (deg i) y)) _,
+    intro x, revert y, refine eq.rec_equiv (deg i) _,
+    apply transport (λx, is_exact_mod x _) (idpath (i' x)),
+    apply transport (λx, is_exact_mod _ (j' ↘ (ap (deg j) (left_inv (deg i) x)))) (idpath x),
+    apply is_exact_mod.mk,
+    { revert x, refine equiv_rect (deg i) _ _, intro x,
+      refine graded_image.rec _, intro m,
+      transitivity j' ↘ _ (graded_image_lift i (deg i x) (i x m)),
+        apply ap (λx, j' ↘ _ x), apply subtype_eq, apply i'_eq,
+      refine !j'_eq ⬝ _,
+      apply ap class_of, apply subtype_eq, exact is_exact.im_in_ker (exact_couple.ij X idp idp) m },
+    { 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,
+      { exact !j'_eq⁻¹ ⬝ p },
+      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) ⬝ _,
+        refine ap (sub _) r ⬝ _, apply sub_self },
+      assert t : trunctype.carrier (image (i ← (deg k x)) (m - k x n)),
+      { exact is_exact.ker_in_im (exact_couple.ij X _ _) _ s },
+      refine image.mk ⟨m - k x n, t⟩ _,
+      apply subtype_eq, refine !i'_eq ⬝ !to_respect_sub ⬝ _,
+      refine ap (sub _) _ ⬝ !sub_zero,
+      apply is_exact.im_in_ker (exact_couple.ki X _ _) }
   end
 
   lemma j'k' : is_exact_gmod j' k' :=
   begin
-    apply is_exact_gmod.mk,
-    { exact sorry },
-    { exact sorry }
+    refine equiv_rect (deg i) _ _,
+    intros x y z p, revert y p z,
+    refine eq.rec_grading (deg i ⬝e deg j') (deg j) (ap (deg j) (left_inv (deg i) x)) _,
+    intro z q, induction q,
+    apply is_exact_mod.mk,
+    { refine graded_image.rec _, intro m,
+      refine ap (k' _) (j'_eq m) ⬝ _,
+      apply subtype_eq,
+      refine k'_eq _ _ ⬝ _,
+      exact is_exact.im_in_ker (exact_couple.jk X idp idp) m },
+    { intro m p, induction m using set_quotient.rec_prop with m,
+      induction m with m h, note q := (k'_eq m h)⁻¹ ⬝ ap pr1 p,
+      induction is_exact.ker_in_im (exact_couple.jk X idp idp) m q with n r,
+      apply image.mk (graded_image_lift i x n),
+      refine !j'_eq ⬝ _,
+      apply ap class_of, apply subtype_eq, exact r }
   end
 
   lemma k'i' : is_exact_gmod k' i' :=
   begin
     apply is_exact_gmod.mk,
-    { intro x m, exact sorry },
-    { exact sorry }
+    { intro x m, induction m using set_quotient.rec_prop with m,
+      cases m with m p, apply subtype_eq,
+      change i (deg k x) (k x m) = 0,
+      exact is_exact.im_in_ker (exact_couple.ki X idp idp) m },
+    { intro x m, induction m with m h, intro p,
+      have i (deg k x) m = 0, from ap pr1 p,
+      induction is_exact.ker_in_im (exact_couple.ki X idp idp) m this with n q,
+      have j (deg k x) m = 0, from @(is_exact.im_in_ker2 (exact_couple.ij X _ _)) m h,
+      have d x n = 0, from ap (j (deg k x)) q ⬝ this,
+      exact image.mk (class_of ⟨n, this⟩) (subtype_eq q) }
   end
 
   end
   end derived_couple
 
-  section
-  open derived_couple exact_couple
+  open derived_couple
 
   definition derived_couple [constructor] {R : Ring} {I : Set}
     (X : exact_couple R I) : exact_couple R I :=
   ⦃exact_couple, D := D' X, E := E' X, i := i' X, j := j' X, k := k' X,
     ij := i'j' X, jk := j'k' X, ki := k'i' X⦄
 
+  /- if an exact couple is bounded, we can prove the convergence theorem for it -/
   structure is_bounded {R : Ring} {I : Set} (X : exact_couple R I) : Type :=
   mk' :: (B B' : I → ℕ)
     (Dub : Π⦃x y⦄ ⦃s : ℕ⦄, (deg (i X))^[s] x = y → B x ≤ s → is_contr (D X y))
@@ -166,7 +226,7 @@ namespace left_module
     (deg_ij_commute : hsquare (deg (j X)) (deg (j X)) (deg (i X)) (deg (i X)))
 
 /- Note: Elb proves Dlb for some bound B', but we want tight control over when B' = 0 -/
-  definition is_bounded.mk [constructor] {R : Ring} {I : Set} {X : exact_couple R I}
+  protected definition is_bounded.mk [constructor] {R : Ring} {I : Set} {X : exact_couple R I}
     (B B' B'' : I → ℕ)
     (Dub : Π⦃x : I⦄ ⦃s : ℕ⦄, B x ≤ s → is_contr (D X ((deg (i X))^[s] x)))
     (Dlb : Π⦃x : I⦄ ⦃s : ℕ⦄, B' x ≤ s → is_surjective (i X (((deg (i X))⁻¹ᵉ^[s + 1] x))))
@@ -184,6 +244,9 @@ namespace left_module
     { assumption }
   end
 
+  namespace convergence_theorem
+  section
+
   open is_bounded
   parameters {R : Ring} {I : Set} (X : exact_couple R I) (HH : is_bounded X)
 
@@ -213,7 +276,7 @@ namespace left_module
     exact Dub !deg_iterate_ik_commute (le.trans !le_max_left h)
   end
 
-  -- we start counting pages at 0, not at 2.
+  -- we start counting pages at 0
   definition page (r : ℕ) : exact_couple R I :=
   iterate derived_couple r X
 
@@ -283,7 +346,8 @@ namespace left_module
   begin
     revert x y z s H p q, induction r with r IH: intro x y z s H p q,
     { exact Dlb p q H },
--- the following is a start of the proof that i is surjective from the contractibility of E
+/- the following is a start of the proof that i is surjective using that E is contractible (but this
+   makes the bound 1 higher than necessary -/
       -- induction p, change is_surjective (i X x),
       -- apply @(is_surjective_of_is_exact_of_is_contr (exact_couple.ij X idp idp)),
       -- refine Elb _ H,
@@ -304,6 +368,7 @@ namespace left_module
     reflexivity
   end
 
+  /- the infinity pages of E and D -/
   definition Einf : graded_module R I :=
   λx, E (page (B3 x)) x
 
@@ -363,6 +428,7 @@ namespace left_module
     { apply ij (page (r n)) }
   end
 
+  /- the convergence theorem is a combination of the following three results -/
   definition short_exact_mod_infpage (n : ℕ) :
     short_exact_mod (Einfdiag n) (Dinfdiag n) (Dinfdiag (n+1)) :=
   begin
@@ -375,11 +441,16 @@ namespace left_module
   definition Dinfdiag0 (bound_zero : B' (deg (k X) x) = 0) : Dinfdiag 0 ≃lm D X (deg (k X) x) :=
   Dinfstable (le_of_eq bound_zero) idp
 
-  definition Dinfdiag_stable {s : ℕ} (h : B (deg (k X) x) ≤ s) : is_contr (Dinfdiag s) :=
+  lemma Dinfdiag_stable {s : ℕ} (h : B (deg (k X) x) ≤ s) : is_contr (Dinfdiag s) :=
   is_contr_D _ _ (Dub !deg_iterate_ik_commute h)
 
   end
+  end convergence_theorem
 
+  -- open convergence_theorem
+  -- print axioms short_exact_mod_infpage
+  -- print axioms Dinfdiag0
+  -- print axioms Dinfdiag_stable
 
 end left_module
 open left_module
@@ -486,7 +557,7 @@ namespace spectrum
     revert t q, refine eq.rec_equiv (add_right_action (- 1)) _,
     induction p using eq.rec_symm,
     apply is_exact_homotopy homotopy.rfl,
-    { symmetry, intro m, exact graded_hom_mk_out_right_inv deg_j_seq_inv⁻¹ᵉ fn_j_sequence m },
+    { symmetry, exact graded_hom_mk_out_destruct deg_j_seq_inv⁻¹ᵉ fn_j_sequence },
     rexact is_exact_of_is_exact_at (is_exact_LES_of_shomotopy_groups (f s) (m, 2)),
   end
 
@@ -496,7 +567,7 @@ namespace spectrum
     revert x y p, refine eq.rec_right_inv (deg j_sequence) _,
     intro x, induction x with n s,
     apply is_exact_homotopy,
-    { symmetry, intro m, exact graded_hom_mk_out_right_inv deg_j_seq_inv⁻¹ᵉ fn_j_sequence m },
+    { symmetry, exact graded_hom_mk_out_destruct deg_j_seq_inv⁻¹ᵉ fn_j_sequence },
     { reflexivity },
     rexact is_exact_of_is_exact_at (is_exact_LES_of_shomotopy_groups (f s) (n, 1)),
   end
diff --git a/algebra/quotient_group.hlean b/algebra/quotient_group.hlean
index dac3721..b4deee0 100644
--- a/algebra/quotient_group.hlean
+++ b/algebra/quotient_group.hlean
@@ -274,12 +274,12 @@ namespace group
     exact H a p,
   end
 
-  definition quotient_group_functor_id {K : subgroup_rel A} (H : Π (a : A), K a → K a) : 
+  definition quotient_group_functor_id {K : subgroup_rel A} (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 
+    end
 
   section quotient_group_iso_ua
 
@@ -311,7 +311,7 @@ namespace group
       fapply is_prop.elim,
     end,
     induction q,
-    reflexivity    
+    reflexivity
   end
 
   definition subgroup_rel_eq {K L : subgroup_rel A} (K_in_L : Π (a : A), K a → L a) (L_in_K : Π (a : A), L a → K a) : K = L :=
@@ -342,26 +342,26 @@ namespace group
   definition htpy_of_ab_qg_group' {K L : subgroup_rel A} (p : K = L) : (iso_of_ab_qg_group' p) ∘g ab_qg_map K ~ ab_qg_map L :=
   begin
     induction p, reflexivity
-  end 
+  end
 
   definition eq_of_ab_qg_group {K L : subgroup_rel A} (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) 
+  eq_of_ab_qg_group' (subgroup_rel_eq K_in_L L_in_K)
 
   definition iso_of_ab_qg_group {K L : subgroup_rel A} (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 : subgroup_rel A} (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' 
+    fapply htpy_of_ab_qg_group'
   end
 
   end quotient_group_iso_ua
-  
+
   section quotient_group_iso
   variables {K L : subgroup_rel A} (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))
@@ -378,7 +378,7 @@ namespace group
     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 : 
+  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)))
 
@@ -394,7 +394,7 @@ namespace group
     end
 -/
 
-  definition quotient_group_iso_contr_aux  : 
+  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,
@@ -403,17 +403,17 @@ namespace group
     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))))),  
+    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)⟩, 
+    -- 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 : subgroup_rel A} (H1 : Π (a : A), K a → L a) (H2 : Π (a : A), L a → K a) : 
+  definition quotient_group_iso_contr {K L : subgroup_rel A} (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), 
+    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) : _
@@ -422,7 +422,7 @@ namespace group
 
   end quotient_group_iso
 
- 
+
   definition quotient_group_functor [constructor] (φ : G →g G') (h : Πg, N g → N' (φ g)) :
     quotient_group N →g quotient_group N' :=
   begin
diff --git a/algebra/submodule.hlean b/algebra/submodule.hlean
index be242cb..301c1e1 100644
--- a/algebra/submodule.hlean
+++ b/algebra/submodule.hlean
@@ -5,7 +5,7 @@
 
 import .left_module .quotient_group
 
-open algebra eq group sigma is_trunc function trunc equiv is_equiv
+open algebra eq group sigma sigma.ops is_trunc function trunc equiv is_equiv
 
 -- move to subgroup
 attribute normal_subgroup_rel._trans_of_to_subgroup_rel [unfold 2]
@@ -122,6 +122,10 @@ lm_homomorphism_of_group_homomorphism (hom_lift (group_homomorphism_of_lm_homomo
     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 :=
+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₂) :
   hom_lift φ h ∘lm ψ ~ hom_lift (φ ∘lm ψ) proof (λm, h (ψ m)) qed :=
@@ -210,6 +214,9 @@ 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 rel_of_quotient_map_eq_zero (m : M) (H : quotient_map S m = 0) : S m :=
+rel_of_qg_map_eq_one m H
+
 definition quotient_elim [constructor] (φ : M →lm M₂) (H : Π⦃m⦄, S m → φ m = 0) :
   quotient_module S →lm M₂ :=
 lm_homomorphism_of_group_homomorphism
@@ -286,6 +293,12 @@ begin
   reflexivity
 end
 
+-- definition image_elim_hom_lift (ψ : M →lm M₂) (h : Π⦃g⦄, φ g = 0 → θ g = 0) :
+--   image_elim θ h ∘lm hom_lift ψ _ ~ _ :=
+-- begin
+--   reflexivity
+-- end
+
 definition is_contr_image_module [instance] (φ : M₁ →lm M₂) [is_contr M₂] :
   is_contr (image_module φ) :=
 !is_contr_submodule
@@ -332,19 +345,19 @@ submodule_isomorphism _ (kernel_rel_full φ)
 definition homology (ψ : M₂ →lm M₃) (φ : M₁ →lm M₂) : LeftModule R :=
 @quotient_module R (submodule (kernel_rel ψ)) (submodule_rel_submodule _ (image_rel φ))
 
-definition homology.mk (m : M₂) (h : ψ m = 0) : homology ψ φ :=
+definition homology.mk (φ : M₁ →lm M₂) (m : M₂) (h : ψ m = 0) : homology ψ φ :=
 quotient_map _ ⟨m, h⟩
 
 definition homology_eq0 {m : M₂} {hm : ψ m = 0} (h : image φ m) :
-  homology.mk m hm = 0 :> homology ψ φ :=
+  homology.mk φ m hm = 0 :=
 ab_qg_map_eq_one _ h
 
 definition homology_eq0' {m : M₂} {hm : ψ m = 0} (h : image φ m):
-  homology.mk m hm = homology.mk 0 (to_respect_zero ψ) :> homology ψ φ :=
+  homology.mk φ m hm = homology.mk φ 0 (to_respect_zero ψ) :=
 ab_qg_map_eq_one _ h
 
 definition homology_eq {m n : M₂} {hm : ψ m = 0} {hn : ψ n = 0} (h : image φ (m - n)) :
-  homology.mk m hm = homology.mk n hn :> homology ψ φ :=
+  homology.mk φ m hm = homology.mk φ n hn :=
 eq_of_sub_eq_zero (homology_eq0 h)
 
 definition homology_elim [constructor] (θ : M₂ →lm M) (H : Πm, θ (φ m) = 0) :
@@ -362,8 +375,8 @@ definition is_contr_homology [instance] (ψ : M₂ →lm M₃) (φ : M₁ →lm
   is_contr (homology ψ φ) :=
 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₂ :=
+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
 
diff --git a/move_to_lib.hlean b/move_to_lib.hlean
index 608d047..6327aef 100644
--- a/move_to_lib.hlean
+++ b/move_to_lib.hlean
@@ -29,6 +29,12 @@ definition is_exact_g.mk {A B C : Group} {f : A →g B} {g : B →g C}
   (H₁ : Πa, g (f a) = 1) (H₂ : Πb, g b = 1 → image f b) : is_exact_g f g :=
 is_exact.mk H₁ H₂
 
+definition is_exact.im_in_ker2 {A B : Type} {C : Set*} {f : A → B} {g : B → C} (H : is_exact f g)
+  {b : B} (h : image f b) : g b = pt :=
+begin
+  induction h with a p, exact ap g p⁻¹ ⬝ is_exact.im_in_ker H a
+end
+
 -- TO DO: give less univalency proof
 definition is_exact_homotopy {A B : Type} {C : Type*} {f f' : A → B} {g g' : B → C}
   (p : f ~ f') (q : g ~ g') (H : is_exact f g) : is_exact f' g' :=
@@ -99,7 +105,7 @@ end algebra
 namespace eq
 
   definition eq.rec_to {A : Type} {a₀ : A} {P : Π⦃a₁⦄, a₀ = a₁ → Type}
-    {a₁ : A} (p₀ : a₀ = a₁) (H : P p₀) {a₂ : A} (p : a₀ = a₂) : P p :=
+    {a₁ : A} (p₀ : a₀ = a₁) (H : P p₀) ⦃a₂ : A⦄ (p : a₀ = a₂) : P p :=
   begin
     induction p₀, induction p, exact H
   end
@@ -125,6 +131,54 @@ namespace eq
     cases qr with q r, apply transport P r, induction q, exact H
   end
 
+  definition eq.rec_equiv_symm {A B : Type} {a₁ : A} (f : A ≃ B) {P : Π{a₀}, f a₀ = f a₁ → Type}
+    (H : P (idpath (f a₁))) ⦃a₀ : A⦄ (p : f a₀ = f a₁) : P p :=
+  begin
+    assert qr : Σ(q : a₀ = a₁), ap f q = p,
+    { exact ⟨eq_of_fn_eq_fn f p, ap_eq_of_fn_eq_fn' f p⟩ },
+    cases qr with q r, apply transport P r, induction q, exact H
+  end
+
+  definition eq.rec_equiv_to_same {A B : Type} {a₀ : A} (f : A ≃ B) {P : Π{a₁}, f a₀ = f a₁ → Type}
+    ⦃a₁' : A⦄ (p' : f a₀ = f a₁') (H : P p') ⦃a₁ : A⦄ (p : f a₀ = f a₁) : P p :=
+  begin
+    revert a₁' p' H a₁ p,
+    refine eq.rec_equiv f _,
+    exact eq.rec_equiv f
+  end
+
+  definition eq.rec_equiv_to {A A' B : Type} {a₀ : A} (f : A ≃ B) (g : A' ≃ B)
+    {P : Π{a₁}, f a₀ = g a₁ → Type}
+    ⦃a₁' : A'⦄ (p' : f a₀ = g a₁') (H : P p') ⦃a₁ : A'⦄ (p : f a₀ = g a₁) : P p :=
+  begin
+    assert qr : Σ(q : g⁻¹ (f a₀) = a₁), (right_inv g (f a₀))⁻¹ ⬝ ap g q = p,
+    { exact ⟨eq_of_fn_eq_fn g (right_inv g (f a₀) ⬝ p),
+             whisker_left _ (ap_eq_of_fn_eq_fn' g _) ⬝ !inv_con_cancel_left⟩ },
+    assert q'r' : Σ(q' : g⁻¹ (f a₀) = a₁'), (right_inv g (f a₀))⁻¹ ⬝ ap g q' = p',
+    { exact ⟨eq_of_fn_eq_fn g (right_inv g (f a₀) ⬝ p'),
+             whisker_left _ (ap_eq_of_fn_eq_fn' g _) ⬝ !inv_con_cancel_left⟩ },
+    induction qr with q r, induction q'r' with q' r',
+    induction q, induction q',
+    induction r, induction r',
+    exact H
+  end
+
+  definition eq.rec_grading {A A' B : Type} {a : A} (f : A ≃ B) (g : A' ≃ B)
+    {P : Π{b}, f a = b → Type}
+    {a' : A'} (p' : f a = g a') (H : P p') ⦃b : B⦄ (p : f a = b) : P p :=
+  begin
+    revert b p, refine equiv_rect g _ _,
+    exact eq.rec_equiv_to f g p' H
+  end
+
+  definition eq.rec_grading_unbased {A B B' C : Type} (f : A ≃ B) (g : B ≃ C) (h : B' ≃ C)
+    {P : Π{b c}, g b = c → Type}
+    {a' : A} {b' : B'} (p' : g (f a') = h b') (H : P p') ⦃b : B⦄ ⦃c : C⦄ (q : f a' = b)
+    (p : g b = c) : P p :=
+  begin
+    induction q, exact eq.rec_grading (f ⬝e g) h p' H p
+  end
+
   definition eq.rec_symm {A : Type} {a₀ : A} {P : Π⦃a₁⦄, a₁ = a₀ → Type}
     (H : P idp) ⦃a₁ : A⦄ (p : a₁ = a₀) : P p :=
   begin
@@ -138,6 +192,12 @@ namespace eq
     apply is_trunc_of_is_contr
   end
 
+  definition cast_fn_cast_square {A : Type} {B C : A → Type} (f : Π⦃a⦄, B a → C a) {a₁ a₂ : A}
+    (p : a₁ = a₂) (q : a₂ = a₁) (r : p ⬝ q = idp) (b : B a₁) :
+    cast (ap C q) (f (cast (ap B p) b)) = f b :=
+  have q⁻¹ = p, from inv_eq_of_idp_eq_con r⁻¹,
+  begin induction this, induction q, reflexivity end
+
 section -- squares
   variables {A B : Type} {a a' a'' a₀₀ a₂₀ a₄₀ a₀₂ a₂₂ a₂₄ a₀₄ a₄₂ a₄₄ a₁ a₂ a₃ a₄ : A}
             /-a₀₀-/ {p₁₀ p₁₀' : a₀₀ = a₂₀} /-a₂₀-/ {p₃₀ : a₂₀ = a₄₀} /-a₄₀-/