diff --git a/algebra/graded.hlean b/algebra/graded.hlean
index 261dcf0..54b2532 100644
--- a/algebra/graded.hlean
+++ b/algebra/graded.hlean
@@ -12,7 +12,7 @@ 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}
+variables {R : Ring} {I : AddGroup} {M M₁ M₂ M₃ : graded_module R I}
 
 /-
   morphisms between graded modules.
@@ -46,17 +46,31 @@ gmd_constant d M₁ M₂
 
 structure graded_hom (M₁ M₂ : graded_module R I) : Type :=
 mk' ::  (d : I ≃ I)
+        (deg_eq : Π(i : I), d i = i + d 0)
         (fn' : graded_hom_of_deg d M₁ M₂)
 
+
+definition deg_eq_id (i : I) : erfl i = i + erfl 0 :=
+!add_zero⁻¹
+
+definition deg_eq_inv {d : I ≃ I} (pd : Π(i : I), d i = i + d 0) (i : I) : d⁻¹ᵉ i = i + d⁻¹ᵉ 0 :=
+inv_eq_of_eq (!pd ⬝ !neg_add_cancel_right)⁻¹ ⬝
+ap (λx, i + x) ((to_left_inv d _)⁻¹ ⬝ ap d⁻¹ᵉ (!pd ⬝ add.left_inv (d 0)))
+
+definition deg_eq_con {d₁ d₂ : I ≃ I} (pd₁ : Π(i : I), d₁ i = i + d₁ 0) (pd₂ : Π(i : I), d₂ i = i + d₂ 0)
+  (i : I) : (d₁ ⬝e d₂) i = i + (d₁ ⬝e d₂) 0 :=
+ap d₂ !pd₁ ⬝ !pd₂ ⬝ !add.assoc ⬝ ap (λx, i + x) !pd₂⁻¹
+
 notation M₁ ` →gm ` M₂ := graded_hom M₁ M₂
 
 abbreviation deg [unfold 5] := @graded_hom.d
+abbreviation deg_eq [unfold 5] := @graded_hom.deg_eq
 postfix ` ↘`:max := graded_hom.fn' -- there is probably a better character for this? Maybe ↷?
 
 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_fn_out [reducible] [unfold 5] (f : M₁ →gm M₂) (i : I) : M₁ ((deg f)⁻¹ i) →lm M₂ i :=
+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 ` ← `:max := graded_hom_fn_out -- todo: change notation
@@ -91,61 +105,65 @@ infix ` ← `:max := graded_hom_fn_out -- todo: change notation
 --   P (f ← i m) :=
 -- graded_hom_fn_out_rec f H m
 
-definition graded_hom.mk [constructor] (d : I ≃ I)
+definition graded_hom.mk [constructor] (d : I ≃ I) (pd : Π(i : I), d i = i + d 0)
   (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)
+graded_hom.mk' d pd (λi j p, homomorphism_of_eq (ap M₂ p) ∘lm fn i)
 
-definition graded_hom.mk_out [constructor] (d : I ≃ I)
+definition graded_hom.mk_out [constructor] (d : I ≃ I) (pd : Π(i : I), d i = i + d 0)
   (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)))
+graded_hom.mk' d pd (λi j p, fn j ∘lm homomorphism_of_eq (ap M₁ (eq_inv_of_eq p)))
 
-definition graded_hom.mk_out' [constructor] (d : I ≃ I)
+definition graded_hom.mk_out' [constructor] (d : I ≃ I) (pd : Π(i : I), d i = i + d 0)
   (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)))
+graded_hom.mk' d⁻¹ᵉ (deg_eq_inv pd) (λi j p, fn j ∘lm homomorphism_of_eq (ap M₁ (eq_inv_of_eq p)))
 
-definition graded_hom.mk_out_in [constructor] (d₁ : I ≃ I) (d₂ : I ≃ I)
+definition graded_hom.mk_out_in [constructor] (d₁ d₂ : I ≃ I)
+  (pd₁ : Π(i : I), d₁ i = i + d₁ 0) (pd₂ : Π(i : I), d₂ i = i + d₂ 0)
   (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)⁻¹))
+graded_hom.mk' (d₁⁻¹ᵉ ⬝e d₂) (deg_eq_con (deg_eq_inv pd₁) pd₂)
+  (λ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_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 :=
+definition graded_hom_mk_refl (d : I ≃ I) (pd : Π(i : I), d i = i + d 0)
+  (fn : Πi, M₁ i →lm M₂ (d i)) {i : I} (m : M₁ i) : graded_hom.mk d pd fn i m = fn i m :=
 by reflexivity
 
-lemma graded_hom_mk_out'_destruct (d : I ≃ I)
+lemma graded_hom_mk_out'_destruct (d : I ≃ I) (pd : Π(i : I), d i = i + d 0)
   (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 :=
+  graded_hom.mk_out' d pd 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 --TODO: we can also prove this if I is not a set
+  apply is_set.elim --note: we can also prove this if I is not a set
 end
 
-lemma graded_hom_mk_out_destruct (d : I ≃ I)
+lemma graded_hom_mk_out_destruct (d : I ≃ I) (pd : Π(i : I), d i = i + d 0)
   (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 :=
+  graded_hom.mk_out d pd fn ↘ (right_inv d i) m = fn i m :=
 begin
-  rexact graded_hom_mk_out'_destruct d⁻¹ᵉ fn m
+  rexact graded_hom_mk_out'_destruct d⁻¹ᵉ (deg_eq_inv pd) fn m
 end
 
 lemma graded_hom_mk_out_in_destruct (d₁ : I ≃ I) (d₂ : I ≃ I)
+  (pd₁ : Π(i : I), d₁ i = i + d₁ 0) (pd₂ : Π(i : I), d₂ i = i + d₂ 0)
   (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 :=
+  graded_hom.mk_out_in d₁ d₂ pd₁ pd₂ 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
 
+variable (I) -- for some reason Lean needs to know what I is when applying this lemma
 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))
+variable {I}
 
 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 :=
@@ -166,7 +184,7 @@ 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 j p, f' ↘ p ∘lm f i)
+graded_hom.mk' (deg f ⬝e deg f') (deg_eq_con (deg_eq f) (deg_eq f')) (λi j p, f' ↘ p ∘lm f i)
 
 infixr ` ∘gm `:75 := graded_hom_compose
 
@@ -188,20 +206,28 @@ definition graded_hom_compose_ext [constructor] (f' : M₂ →gm M₃) (f : 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)))
+graded_hom.mk' (deg f ⬝e deg f') (deg_eq_con (deg_eq f) (deg_eq f')) (λi j p, (f' ↘ (pf' p)) ∘lm (f ↘ (pf p)))
 
 variable (M)
 definition graded_hom_id [constructor] [refl] : M →gm M :=
-graded_hom.mk erfl (λi, lmid)
+graded_hom.mk erfl deg_eq_id (λi, lmid)
 variable {M}
 abbreviation gmid [constructor] := graded_hom_id M
 
-definition graded_hom_reindex [constructor] {J : Set} (e : J ≃ I) (f : M₁ →gm M₂) :
+/- reindexing a graded morphism along a group homomorphism.
+  We could also reindex along an affine transformation, but don't prove that here
+-/
+definition graded_hom_reindex [constructor] {J : AddGroup} (e : J ≃g I) (f : M₁ →gm M₂) :
   (λy, M₁ (e y)) →gm (λy, M₂ (e y)) :=
-graded_hom.mk' (e ⬝e deg f ⬝e e⁻¹ᵉ) (λy₁ y₂ p, f ↘ (eq_of_inv_eq p))
+graded_hom.mk' (group.equiv_of_isomorphism e ⬝e deg f ⬝e (group.equiv_of_isomorphism e)⁻¹ᵉ)
+  begin intro i, exact ap e⁻¹ᵍ (deg_eq f (e i)) ⬝ respect_add e⁻¹ᵍ _ _ ⬝
+    ap011 add (to_left_inv (group.equiv_of_isomorphism e) i)
+              (ap (e⁻¹ᵍ ∘ deg f) (respect_zero e)⁻¹) end
+  (λy₁ y₂ p, f ↘ (to_eq_of_inv_eq (group.equiv_of_isomorphism e) p))
 
-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₂)
+definition gm_constant [constructor] (M₁ M₂ : graded_module R I) (d : I ≃ I) (pd : Π(i : I), d i = i + d 0)
+   (pd : Π(i : I), d i = i + d 0) : M₁ →gm M₂ :=
+graded_hom.mk' d pd (gmd_constant d M₁ M₂)
 
 definition is_surjective_graded_hom_compose ⦃x z⦄
   (f' : M₂ →gm M₃) (f : M₁ →gm M₂) (p : deg f' (deg f x) = z)
@@ -234,28 +260,29 @@ definition isomorphism_of_graded_iso [constructor] (φ : M₁ ≃gm M₂) (i : I
 isomorphism.mk (φ i) _
 
 definition isomorphism_of_graded_iso_out [constructor] (φ : M₁ ≃gm M₂) (i : I) :
-  M₁ ((deg φ)⁻¹ i) ≃lm M₂ i :=
-isomorphism_of_graded_iso' φ !to_right_inv
+  M₁ ((deg φ)⁻¹ᵉ i) ≃lm M₂ i :=
+isomorphism_of_graded_iso' φ (to_right_inv (deg φ) i)
 
-protected definition graded_iso.mk [constructor] (d : I ≃ I) (φ : Πi, M₁ i ≃lm M₂ (d i)) :
-  M₁ ≃gm M₂ :=
+protected definition graded_iso.mk [constructor] (d : I ≃ I)  (pd : Π(i : I), d i = i + d 0)
+  (φ : Πi, M₁ i ≃lm M₂ (d i)) : M₁ ≃gm M₂ :=
 begin
-  apply graded_iso.mk' (graded_hom.mk d φ),
+  apply graded_iso.mk' (graded_hom.mk d pd φ),
   intro i j p, induction p,
   exact to_is_equiv (equiv_of_isomorphism (φ i)),
 end
 
-protected definition graded_iso.mk_out [constructor] (d : I ≃ I) (φ : Πi, M₁ (d⁻¹ i) ≃lm M₂ i) :
+protected definition graded_iso.mk_out [constructor] (d : I ≃ I)
+   (pd : Π(i : I), d i = i + d 0) (φ : Πi, M₁ (d⁻¹ i) ≃lm M₂ i) :
   M₁ ≃gm M₂ :=
 begin
-  apply graded_iso.mk' (graded_hom.mk_out d φ),
+  apply graded_iso.mk' (graded_hom.mk_out d pd φ),
   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.mk erfl (λi, isomorphism_of_eq (p i))
+graded_iso.mk erfl deg_eq_id (λi, isomorphism_of_eq (p i))
 
 -- definition to_gminv [constructor] (φ : M₁ ≃gm M₂) : M₂ →gm M₁ :=
 -- graded_hom.mk_out (deg φ)⁻¹ᵉ
@@ -266,16 +293,16 @@ graded_iso.mk erfl (λi, isomorphism_of_eq (p i))
 
 variable (M)
 definition graded_iso.refl [refl] [constructor] : M ≃gm M :=
-graded_iso.mk equiv.rfl (λi, isomorphism.rfl)
+graded_iso.mk equiv.rfl deg_eq_id (λ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_out (deg φ)⁻¹ᵉ (λi, (isomorphism_of_graded_iso φ i)⁻¹ˡᵐ)
+graded_iso.mk_out (deg φ)⁻¹ᵉ (deg_eq_inv (deg_eq φ)) (λi, (isomorphism_of_graded_iso φ i)⁻¹ˡᵐ)
 
 definition graded_iso.trans [trans] [constructor] (φ : M₁ ≃gm M₂) (ψ : M₂ ≃gm M₃) : M₁ ≃gm M₃ :=
-graded_iso.mk (deg φ ⬝e deg ψ)
+graded_iso.mk (deg φ ⬝e deg ψ) (deg_eq_con (deg_eq φ) (deg_eq ψ))
   (λi, isomorphism_of_graded_iso φ i ⬝lm isomorphism_of_graded_iso ψ (deg φ i))
 
 definition graded_iso.eq_trans [trans] [constructor]
@@ -298,7 +325,7 @@ definition fooff {I : Set} (P : I → Type) {i j : I} (M : P i) (N : P j) := uni
 notation M ` ==[`:50 P:0 `] `:0 N:50 := fooff P M N
 
 definition graded_homotopy (f g : M₁ →gm M₂) : Type :=
-Π⦃i j k⦄ (p : deg f i = j) (q : deg g i = k) (m : M₁ i), f ↘ p m ==[λi, M₂ i] g ↘ q m
+Π⦃i j k⦄ (p : deg f i = j) (q : deg g i = k) (m : M₁ i), f ↘ p m ==[λ(i : Set_of_AddGroup I), M₂ i] g ↘ q m
 -- mk' :: (hd : deg f ~ deg g)
 --        (hfn : Π⦃i j : I⦄ (pf : deg f i = j) (pg : deg g i = j), f ↘ pf ~ g ↘ pg)
 
@@ -311,7 +338,7 @@ infix ` ~gm `:50 := graded_homotopy
 --     exact graded_hom_eq_transport f (hd i) m ⬝ tr_eq_of_pathover (hfn i m),
 --   end
 
-definition graded_homotopy.mk (h : Πi m, f i m ==[λi, M₂ i] g i m) : f ~gm g :=
+definition graded_homotopy.mk (h : Πi m, f i m ==[λ(i : Set_of_AddGroup I), M₂ i] g i m) : f ~gm g :=
 begin
   intros i j k p q m, induction q, induction p, constructor --exact h i m
 end
@@ -432,12 +459,12 @@ definition graded_submodule [constructor] (S : Πi, property (M i)) [Π i, is_su
 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))
+graded_hom.mk erfl deg_eq_id (λi, submodule_incl (S 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), φ i m ∈ S (deg φ i)) : M₁ →gm graded_submodule S :=
-graded_hom.mk (deg φ) (λi, hom_lift (φ i) (h i))
+graded_hom.mk (deg φ) (deg_eq φ) (λi, hom_lift (φ i) (h i))
 
 definition graded_submodule_functor [constructor]
   {S : Πi, property (M₁ i)} [Π i, is_submodule (M₁ i) (S i)]
@@ -445,7 +472,7 @@ definition graded_submodule_functor [constructor]
   (φ : 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))
+graded_hom.mk (deg φ) (deg_eq φ) (λi, submodule_functor (φ i) (h i))
 
 definition graded_image (f : M₁ →gm M₂) : graded_module R I :=
 λi, image_module (f ← i)
@@ -455,7 +482,7 @@ lemma graded_image_lift_lemma (f : M₁ →gm M₂) {i j: I} (p : deg f i = j) (
 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' (deg f) (λi j p, hom_lift (f ↘ p) (graded_image_lift_lemma f p))
+graded_hom.mk' (deg f) (deg_eq 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 :=
@@ -488,18 +515,19 @@ 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_helper {f : M₁ →gm M₂} (g : M₁ →gm M₃)
+  (h : Π⦃i m⦄, f i m = 0 → g i m = 0) (i : I) : graded_image f (deg f i) →lm M₃ (deg g i) :=
+begin
+  apply image_elim (g ↘ (ap (deg g) (to_left_inv (deg f) i))),
+  intro m p,
+  refine graded_hom_eq_zero I m (h _),
+  exact graded_hom_eq_zero I m p
+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_out_in (deg f) (deg g),
-  intro i,
-  apply image_elim (g ↘ (ap (deg g) (to_left_inv (deg f) i))),
-  exact abstract begin
-    intro m p,
-    refine graded_hom_eq_zero m (h _),
-    exact graded_hom_eq_zero m p end end
-end
+graded_hom.mk_out_in (deg f) (deg g) (deg_eq f) (deg_eq g) (graded_image_elim_helper g h)
 
 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}
@@ -517,7 +545,8 @@ begin
     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 graded_hom_mk_out_in_destruct (deg f) (deg g) (deg_eq f) (deg_eq g)
+           (graded_image_elim_helper g h) (graded_image_lift f ← (deg f i) m) ⬝ _,
   refine ap (image_elim _ _) !graded_image_lift_destruct ⬝ _, reflexivity
 end
 
@@ -601,13 +630,13 @@ definition graded_quotient (S : Πi, property (M i)) [Π i, is_submodule (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))
+graded_hom.mk erfl deg_eq_id (λi, quotient_map (S i))
 
 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))
+graded_hom.mk (deg φ) (deg_eq φ) (λi, quotient_elim (φ i) (H i))
 
 definition graded_homology (g : M₂ →gm M₃) (f : M₁ →gm M₂) : graded_module R I :=
 graded_quotient (λ i, homology_quotient_property (g i) (f ← i))
@@ -626,7 +655,7 @@ definition graded_homology_intro [constructor] (g : M₂ →gm M₃) (f : M₁ 
 
 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 _ _))
+graded_hom.mk (deg h) (deg_eq h) (λi, homology_elim (h i) (H _ _))
 
 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) :
@@ -651,9 +680,17 @@ definition gmod_ker_in_im (h : is_exact_gmod f f') ⦃i : I⦄ (m : M₂ i) (p :
   image (f ← i) m :=
 is_exact.ker_in_im (h (right_inv (deg f) i) idp) m p
 
-definition is_exact_gmod_reindex [constructor] {J : Set} (e : J ≃ I) (h : is_exact_gmod f f') :
+definition is_exact_gmod_reindex [constructor] {J : AddGroup} (e : J ≃g I) (h : is_exact_gmod f f') :
   is_exact_gmod (graded_hom_reindex e f) (graded_hom_reindex e f') :=
 λi j k p q, h (eq_of_inv_eq p) (eq_of_inv_eq q)
 
+definition deg_commute {I : AddAbGroup} {M₁ M₂ M₃ M₄ : graded_module R I} (f : M₁ →gm M₂)
+  (g : M₃ →gm M₄) : hsquare (deg f) (deg f) (deg g) (deg g) :=
+begin
+  intro i,
+  refine ap (deg g) (deg_eq f i) ⬝ deg_eq g _ ⬝ _ ⬝ (ap (deg f) (deg_eq g i) ⬝ deg_eq f _)⁻¹,
+  exact !add.assoc ⬝ ap (λx, i + x) !add.comm ⬝ !add.assoc⁻¹
+end
+
 
 end left_module
diff --git a/algebra/spectral_sequence.hlean b/algebra/spectral_sequence.hlean
index c2cb563..d1af0f8 100644
--- a/algebra/spectral_sequence.hlean
+++ b/algebra/spectral_sequence.hlean
@@ -7,7 +7,7 @@
 
 import .graded ..spectrum.basic .product_group
 
-open algebra is_trunc left_module is_equiv equiv eq function nat sigma set_quotient
+open algebra is_trunc left_module is_equiv equiv eq function nat sigma set_quotient group
 
 /- exact couples -/
 
@@ -71,7 +71,7 @@ namespace left_module
 
   end
 
-  structure exact_couple (R : Ring) (I : Set) : Type :=
+  structure exact_couple (R : Ring) (I : AddAbGroup) : Type :=
     (D E : graded_module R I)
     (i : D →gm D) (j : D →gm E) (k : E →gm D)
     (ij : is_exact_gmod i j)
@@ -80,17 +80,21 @@ namespace left_module
 
   open exact_couple
 
-  definition exact_couple_reindex [constructor] {R : Ring} {I J : Set} (e : J ≃ I)
+  definition exact_couple_reindex [constructor] {R : Ring} {I J : AddAbGroup}
+    (e : AddGroup_of_AddAbGroup J ≃g AddGroup_of_AddAbGroup I)
     (X : exact_couple R I) : exact_couple R J :=
   ⦃exact_couple, D := λy, D X (e y), E := λy, E X (e y),
-    i := graded_hom_reindex e (i X), j := graded_hom_reindex e (j X),
-    k := graded_hom_reindex e (k X), ij := is_exact_gmod_reindex e (ij X),
-    jk := is_exact_gmod_reindex e (jk X), ki := is_exact_gmod_reindex e (ki X)⦄
+    i := graded_hom_reindex e (i X),
+    j := graded_hom_reindex e (j X),
+    k := graded_hom_reindex e (k X),
+    ij := is_exact_gmod_reindex e (ij X),
+    jk := is_exact_gmod_reindex e (jk X),
+    ki := is_exact_gmod_reindex e (ki X)⦄
 
   namespace derived_couple
   section
 
-  parameters {R : Ring} {I : Set} (X : exact_couple R I)
+  parameters {R : Ring} {I : AddAbGroup} (X : exact_couple R I)
   local abbreviation D := D X
   local abbreviation E := E X
   local abbreviation i := i X
@@ -279,68 +283,61 @@ namespace left_module
 
   open derived_couple
 
-  definition derived_couple [constructor] {R : Ring} {I : Set}
+  definition derived_couple [constructor] {R : Ring} {I : AddAbGroup}
     (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 :=
+  structure is_bounded {R : Ring} {I : AddAbGroup} (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))
     (Dlb : Π⦃x y z⦄ ⦃s : ℕ⦄ (p : deg (i X) x = y), (deg (i X))^[s] y = z → B' z ≤ s → is_surjective (i X ↘ p))
     (Elb : Π⦃x y⦄ ⦃s : ℕ⦄, (deg (i X))⁻¹ᵉ^[s] x = y → B x ≤ s → is_contr (E X y))
-    (deg_ik_commute : hsquare (deg (k X)) (deg (k X)) (deg (i X)) (deg (i X)))
-    (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 -/
-  protected definition is_bounded.mk [constructor] {R : Ring} {I : Set} {X : exact_couple R I}
+  protected definition is_bounded.mk [constructor] {R : Ring} {I : AddAbGroup} {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))))
-    (Elb : Π⦃x : I⦄ ⦃s : ℕ⦄, B'' x ≤ s → is_contr (E X ((deg (i X))⁻¹ᵉ^[s] x)))
-    (deg_ik_commute : hsquare (deg (k X)) (deg (k X)) (deg (i X)) (deg (i X)))
-    (deg_ij_commute : hsquare (deg (j X)) (deg (j X)) (deg (i X)) (deg (i X))) : is_bounded X :=
+    (Elb : Π⦃x : I⦄ ⦃s : ℕ⦄, B'' x ≤ s → is_contr (E X ((deg (i X))⁻¹ᵉ^[s] x))) : is_bounded X :=
   begin
     apply is_bounded.mk' (λx, max (B x) (B'' x)) B',
     { intro x y s p h, induction p, exact Dub (le.trans !le_max_left h) },
     { exact abstract begin intro x y z s p q h, induction p, induction q,
       refine transport (λx, is_surjective (i X x)) _ (Dlb h),
       rewrite [-iterate_succ], apply iterate_left_inv end end },
-    { intro x y s p h, induction p, exact Elb (le.trans !le_max_right h) },
-    { assumption },
-    { assumption }
+    { intro x y s p h, induction p, exact Elb (le.trans !le_max_right h) }
   end
 
   open is_bounded
-  definition is_bounded_reindex [constructor] {R : Ring} {I J : Set} (e : J ≃ I)
+  definition is_bounded_reindex [constructor] {R : Ring} {I J : AddAbGroup}
+    (e : AddGroup_of_AddAbGroup J ≃g AddGroup_of_AddAbGroup I)
     {X : exact_couple R I} (HH : is_bounded X) : is_bounded (exact_couple_reindex e X) :=
   begin
     apply is_bounded.mk' (B HH ∘ e) (B' HH ∘ e),
     { intros x y s p h, refine Dub HH _ h,
-      refine (iterate_hsquare e _ s x)⁻¹ ⬝ ap e p, intro x, exact to_right_inv e _ },
+      refine (iterate_hsquare e _ s x)⁻¹ ⬝ ap e p, intro x,
+      exact to_right_inv (group.equiv_of_isomorphism e) _ },
     { intros x y z s p q h, refine Dlb HH _ _ h,
-      refine (iterate_hsquare e _ s y)⁻¹ ⬝ ap e q, intro x, exact to_right_inv e _ },
+      refine (iterate_hsquare e _ s y)⁻¹ ⬝ ap e q, intro x,
+      exact to_right_inv (group.equiv_of_isomorphism e) _ },
     { intro x y s p h, refine Elb HH _ h,
-      refine (iterate_hsquare e _ s x)⁻¹ ⬝ ap e p, intro x, exact to_right_inv e _ },
-    { intro y, exact ap e⁻¹ᵉ (ap (deg (i X)) (to_right_inv e _) ⬝
-        deg_ik_commute HH (e y) ⬝ ap (deg (k X)) (to_right_inv e _)⁻¹) },
-    { intro y, exact ap e⁻¹ᵉ (ap (deg (i X)) (to_right_inv e _) ⬝
-        deg_ij_commute HH (e y) ⬝ ap (deg (j X)) (to_right_inv e _)⁻¹) }
+      refine (iterate_hsquare e _ s x)⁻¹ ⬝ ap e p, intro x,
+      exact to_right_inv (group.equiv_of_isomorphism e) _ },
+
   end
 
   namespace convergence_theorem
   section
 
-  parameters {R : Ring} {I : Set} (X : exact_couple R I) (HH : is_bounded X)
+  parameters {R : Ring} {I : AddAbGroup} (X : exact_couple R I) (HH : is_bounded X)
 
   local abbreviation B := B HH
   local abbreviation B' := B' HH
   local abbreviation Dub := Dub HH
   local abbreviation Dlb := Dlb HH
   local abbreviation Elb := Elb HH
-  local abbreviation deg_ik_commute := deg_ik_commute HH
-  local abbreviation deg_ij_commute := deg_ij_commute HH
 
   /- We start counting pages at 0, which corresponds to what is usually called the second page -/
   definition page (r : ℕ) : exact_couple R I :=
@@ -415,11 +412,11 @@ namespace left_module
 
   definition deg_iterate_ik_commute (n : ℕ) :
     hsquare (deg (k X)) (deg (k X)) ((deg (i X))^[n]) ((deg (i X))^[n]) :=
-  iterate_commute n deg_ik_commute
+  iterate_commute n (deg_commute (k X) (i X))
 
   definition deg_iterate_ij_commute (n : ℕ) :
     hsquare (deg (j X)) (deg (j X)) ((deg (i X))⁻¹ᵉ^[n]) ((deg (i X))⁻¹ᵉ^[n]) :=
-  iterate_commute n (hvinverse deg_ij_commute)
+  iterate_commute n (deg_commute (j X) (i X))⁻¹ʰᵗʸᵛ
 
   definition B2 (x : I) : ℕ := max (B (deg (k X) x)) (B ((deg (j X))⁻¹ x))
   definition Eub ⦃x y : I⦄ ⦃s : ℕ⦄ (p : (deg (i X))^[s] x = y) (h : B2 x ≤ s) :
@@ -427,8 +424,8 @@ namespace left_module
   begin
     induction p,
     refine @(is_contr_middle_of_is_exact (exact_couple.jk X (right_inv (deg (j X)) _) idp)) _ _ _,
-    exact Dub (iterate_commute s (hhinverse deg_ij_commute) x) (le.trans !le_max_right h),
-    exact Dub !deg_iterate_ik_commute (le.trans !le_max_left h)
+    exact Dub (iterate_commute s (deg_commute (j X) (i X))⁻¹ʰᵗʸʰ x) (le.trans !le_max_right h),
+    exact Dub (deg_iterate_ik_commute s x) (le.trans !le_max_left h)
   end
 
   definition B3 (x : I) : ℕ :=
@@ -549,7 +546,7 @@ namespace left_module
     refine short_exact_mod_isomorphism _ _ _ (short_exact_mod_page_r n),
     { exact Einfstable !rb2 idp },
     { exact Dinfstable !rb3 !deg_k },
-    { exact Dinfstable !rb4 (!deg_i ⬝ ap (deg (i X)) !deg_k ⬝ !deg_ik_commute) }
+    { exact Dinfstable !rb4 (!deg_i ⬝ ap (deg (i X)) !deg_k ⬝ deg_commute (k X) (i X) _) }
   end
 
   definition Dinfdiag0 (bound_zero : B' (deg (k X) x) = 0) : Dinfdiag 0 ≃lm D X (deg (k X) x) :=
@@ -580,68 +577,76 @@ namespace left_module
 
   open int group prod convergence_theorem prod.ops
 
-  definition Z2 [constructor] : Set := gℤ ×g gℤ
+  definition Z2 [constructor] : AddAbGroup := agℤ ×ag agℤ
+
+  -- set_option pp.coercions true
+  -- set_option pp.binder_types true
+
+  -- todo: move
+  definition AddAbGroup.struct2 [instance] (G : AddAbGroup) :
+    add_ab_group (algebra._trans_of_Group_of_AbGroup_2 G) :=
+  AddAbGroup.struct G
 
   /- TODO: redefine/generalize converges_to so that it supports the usual indexing on ℤ × ℤ -/
-  structure converges_to.{u v w} {R : Ring} (E' : gℤ → gℤ → LeftModule.{u v} R)
-                                 (Dinf : gℤ → LeftModule.{u w} R) : Type.{max u (v+1) (w+1)} :=
+  structure converges_to.{u v w} {R : Ring} (E' : agℤ → agℤ → LeftModule.{u v} R)
+                                 (Dinf : agℤ → LeftModule.{u w} R) : Type.{max u (v+1) (w+1)} :=
     (X : exact_couple.{u 0 w v} R Z2)
     (HH : is_bounded X)
-    (s₀ : gℤ → gℤ)
-    (HB : Π(n : gℤ), is_bounded.B' HH (deg (k X) (n, s₀ n)) = 0)
+    (s₀ : agℤ → agℤ)
+    (HB : Π(n : agℤ), is_bounded.B' HH (deg (k X) (n, s₀ n)) = 0)
     (e : Π(x : Z2), exact_couple.E X x ≃lm E' x.1 x.2)
-    (f : Π(n : gℤ), exact_couple.D X (deg (k X) (n, s₀ n)) ≃lm Dinf n)
-    (deg_d1 : ℕ → gℤ) (deg_d2 : ℕ → gℤ)
-    (deg_d_eq : Π(r : ℕ) (n s : gℤ), deg (d (page X r)) (n, s) = (n + deg_d1 r, s + deg_d2 r))
+    (f : Π(n : agℤ), exact_couple.D X (deg (k X) (n, s₀ n)) ≃lm Dinf n)
+    (deg_d1 : ℕ → agℤ) (deg_d2 : ℕ → agℤ)
+    (deg_d_eq : Π(r : ℕ) (n s : agℤ), deg (d (page X r)) (n, s) = (n, s) + (deg_d1 r, deg_d2 r))
 
-  structure converging_spectral_sequence.{u v w} {R : Ring} (E' : gℤ → gℤ → LeftModule.{u v} R)
-                                 (Dinf : gℤ → LeftModule.{u w} R) : Type.{max u (v+1) (w+1)} :=
+  structure converging_spectral_sequence.{u v w} {R : Ring} (E' : agℤ → agℤ → LeftModule.{u v} R)
+                                 (Dinf : agℤ → LeftModule.{u w} R) : Type.{max u (v+1) (w+1)} :=
     (E : ℕ → graded_module.{u 0 v} R Z2)
     (d : Π(n : ℕ), E n →gm E n)
     (α : Π(n : ℕ) (x : Z2), E (n+1) x ≃lm graded_homology (d n) (d n) x)
     (e : Π(n : ℕ) (x : Z2), E 0 x ≃lm E' x.1 x.2)
     (s₀ : Z2 → ℕ)
     (f : Π{n : ℕ} {x : Z2} (h : s₀ x ≤ n), E (s₀ x) x ≃lm E n x)
-    (HDinf : Π(n : gℤ), is_built_from (Dinf n) (λ(k : ℕ), (λx, E (s₀ x) x) (k, n - k)))
+    (HDinf : Π(n : agℤ), is_built_from (Dinf n) (λ(k : ℕ), (λx, E (s₀ x) x) (k, n - k)))
 
   infix ` ⟹ `:25 := converges_to
 
-  definition converges_to_g [reducible] (E' : gℤ → gℤ → AbGroup) (Dinf : gℤ → AbGroup) : Type :=
+  definition converges_to_g [reducible] (E' : agℤ → agℤ → AbGroup) (Dinf : agℤ → AbGroup) : Type :=
   (λn s, LeftModule_int_of_AbGroup (E' n s)) ⟹ (λn, LeftModule_int_of_AbGroup (Dinf n))
 
   infix ` ⟹ᵍ `:25 := converges_to_g
 
   section
   open converges_to
-  parameters {R : Ring} {E' : gℤ → gℤ → LeftModule R} {Dinf : gℤ → LeftModule R} (c : E' ⟹ Dinf)
+  parameters {R : Ring} {E' : agℤ → agℤ → LeftModule R} {Dinf : agℤ → LeftModule R} (c : E' ⟹ Dinf)
   local abbreviation X := X c
   local abbreviation i := i X
   local abbreviation HH := HH c
   local abbreviation s₀ := s₀ c
-  local abbreviation Dinfdiag (n : gℤ) (k : ℕ) := Dinfdiag HH (n, s₀ n) k
-  local abbreviation Einfdiag (n : gℤ) (k : ℕ) := Einfdiag HH (n, s₀ n) k
+  local abbreviation Dinfdiag (n : agℤ) (k : ℕ) := Dinfdiag HH (n, s₀ n) k
+  local abbreviation Einfdiag (n : agℤ) (k : ℕ) := Einfdiag HH (n, s₀ n) k
 
-  definition deg_d_inv_eq (r : ℕ) (n s : gℤ) :
+  definition deg_d_inv_eq (r : ℕ) (n s : agℤ) :
     (deg (d (page X r)))⁻¹ᵉ (n, s) = (n - deg_d1 c r, s - deg_d2 c r) :=
   inv_eq_of_eq (!deg_d_eq ⬝ prod_eq !sub_add_cancel !sub_add_cancel)⁻¹
 
-  definition converges_to_isomorphism {E'' : gℤ → gℤ → LeftModule R} {Dinf' : graded_module R gℤ}
+  definition converges_to_isomorphism {E'' : agℤ → agℤ → LeftModule R} {Dinf' : graded_module R agℤ}
     (e' : Πn s, E' n s ≃lm E'' n s) (f' : Πn, Dinf n ≃lm Dinf' n) : E'' ⟹ Dinf' :=
   converges_to.mk X HH s₀ (HB c)
     begin intro x, induction x with n s, exact e c (n, s) ⬝lm e' n s end
     (λn, f c n ⬝lm f' n)
     (deg_d1 c) (deg_d2 c) (λr n s, deg_d_eq c r n s)
 
-/-  definition converges_to_reindex {E'' : gℤ → gℤ → LeftModule R} {Dinf' : graded_module R gℤ}
-    (i : gℤ ×g gℤ ≃ gℤ × gℤ) (e' : Πp q, E' p q ≃lm E'' (i (p, q)).1 (i (p, q)).2)
-    (i2 : gℤ ≃ gℤ) (f' : Πn, Dinf n ≃lm Dinf' (i2 n)) :
+/-  definition converges_to_reindex {E'' : agℤ → agℤ → LeftModule R} {Dinf' : graded_module R agℤ}
+    (i : agℤ ×g agℤ ≃ agℤ × agℤ) (e' : Πp q, E' p q ≃lm E'' (i (p, q)).1 (i (p, q)).2)
+    (i2 : agℤ ≃ agℤ) (f' : Πn, Dinf n ≃lm Dinf' (i2 n)) :
     (λp q, E'' p q) ⟹ λn, Dinf' n :=
   converges_to.mk (exact_couple_reindex i X) (is_bounded_reindex i HH) s₀
     sorry --(λn, ap (B' HH) (to_right_inv i _ ⬝ begin end) ⬝ HB c n)
     sorry --begin intro x, induction x with p q, exact e c (p, q) ⬝lm e' p q end
     sorry-/
 
-/-  definition converges_to_reindex_neg {E'' : gℤ → gℤ → LeftModule R} {Dinf' : graded_module R gℤ}
+/-  definition converges_to_reindex_neg {E'' : agℤ → agℤ → LeftModule R} {Dinf' : graded_module R agℤ}
     (e' : Πp q, E' p q ≃lm E'' (-p) (-q))
     (f' : Πn, Dinf n ≃lm Dinf' (-n)) :
     (λp q, E'' p q) ⟹ λn, Dinf' n :=
@@ -655,8 +660,8 @@ namespace left_module
   is_built_from_isomorphism_left (f c n) (is_built_from_infpage HH (n, s₀ n) (HB c n))
 
   /- TODO: reprove this using is_built_of -/
-  theorem is_contr_converges_to_precise (n : gℤ)
-  (H : Π(n : gℤ) (l : ℕ), is_contr (E' ((deg i)^[l] (n, s₀ n)).1 ((deg i)^[l] (n, s₀ n)).2)) :
+  theorem is_contr_converges_to_precise (n : agℤ)
+  (H : Π(n : agℤ) (l : ℕ), is_contr (E' ((deg i)^[l] (n, s₀ n)).1 ((deg i)^[l] (n, s₀ n)).2)) :
     is_contr (Dinf n) :=
   begin
     assert H2 : Π(l : ℕ), is_contr (Einfdiag n l),
@@ -673,30 +678,30 @@ namespace left_module
     exact equiv_of_isomorphism (Dinfdiag0 HH (n, s₀ n) (HB c n) ⬝lm f c n)
   end
 
-  theorem is_contr_converges_to (n : gℤ) (H : Π(n s : gℤ), is_contr (E' n s)) : is_contr (Dinf n) :=
+  theorem is_contr_converges_to (n : agℤ) (H : Π(n s : agℤ), is_contr (E' n s)) : is_contr (Dinf n) :=
   is_contr_converges_to_precise n (λn s, !H)
 
-  definition E_isomorphism {r₁ r₂ : ℕ} {n s : gℤ} (H : r₁ ≤ r₂)
+  definition E_isomorphism {r₁ r₂ : ℕ} {n s : agℤ} (H : r₁ ≤ r₂)
     (H1 : Π⦃r⦄, r₁ ≤ r → r < r₂ → is_contr (E X (n - deg_d1 c r, s - deg_d2 c r)))
     (H2 : Π⦃r⦄, r₁ ≤ r → r < r₂ → is_contr (E X (n + deg_d1 c r, s + deg_d2 c r))) :
     E (page X r₂) (n, s) ≃lm E (page X r₁) (n, s) :=
   E_isomorphism' X H (λr Hr₁ Hr₂, transport (is_contr ∘ E X) (deg_d_inv_eq r n s)⁻¹ᵖ (H1 Hr₁ Hr₂))
                     (λr Hr₁ Hr₂, transport (is_contr ∘ E X) (deg_d_eq c r n s)⁻¹ᵖ (H2 Hr₁ Hr₂))
 
-  definition E_isomorphism0 {r : ℕ} {n s : gℤ}
+  definition E_isomorphism0 {r : ℕ} {n s : agℤ}
     (H1 : Πr, is_contr (E X (n - deg_d1 c r, s - deg_d2 c r)))
     (H2 : Πr, is_contr (E X (n + deg_d1 c r, s + deg_d2 c r))) :
     E (page X r) (n, s) ≃lm E' n s :=
   E_isomorphism (zero_le r) _ _ ⬝lm e c (n, s)
 
-  definition Einf_isomorphism (r₁ : ℕ) {n s : gℤ}
+  definition Einf_isomorphism (r₁ : ℕ) {n s : agℤ}
     (H1 : Π⦃r⦄, r₁ ≤ r → is_contr (E X (n - deg_d1 c r, s - deg_d2 c r)))
     (H2 : Π⦃r⦄, r₁ ≤ r → is_contr (E X (n + deg_d1 c r, s + deg_d2 c r))) :
     Einf HH (n, s) ≃lm E (page X r₁) (n, s) :=
   Einf_isomorphism' HH r₁ (λr Hr₁, transport (is_contr ∘ E X) (deg_d_inv_eq r n s)⁻¹ᵖ (H1 Hr₁))
                          (λr Hr₁, transport (is_contr ∘ E X) (deg_d_eq c r n s)⁻¹ᵖ (H2 Hr₁))
 
-  definition Einf_isomorphism0 {n s : gℤ}
+  definition Einf_isomorphism0 {n s : agℤ}
     (H1 : Π⦃r⦄, is_contr (E X (n - deg_d1 c r, s - deg_d2 c r)))
     (H2 : Π⦃r⦄, is_contr (E X (n + deg_d1 c r, s + deg_d2 c r))) :
     Einf HH (n, s) ≃lm E' n s :=
@@ -704,8 +709,8 @@ namespace left_module
 
   end
 
-  variables {E' : gℤ → gℤ → AbGroup} {Dinf : gℤ → AbGroup} (c : E' ⟹ᵍ Dinf)
-  definition converges_to_g_isomorphism {E'' : gℤ → gℤ → AbGroup} {Dinf' : gℤ → AbGroup}
+  variables {E' : agℤ → agℤ → AbGroup} {Dinf : agℤ → AbGroup} (c : E' ⟹ᵍ Dinf)
+  definition converges_to_g_isomorphism {E'' : agℤ → agℤ → AbGroup} {Dinf' : agℤ → AbGroup}
     (e' : Πn s, E' n s ≃g E'' n s) (f' : Πn, Dinf n ≃g Dinf' n) : E'' ⟹ᵍ Dinf' :=
   converges_to_isomorphism c (λn s, lm_iso_int.mk (e' n s)) (λn, lm_iso_int.mk (f' n))
 
@@ -768,7 +773,6 @@ namespace spectrum
 
   parameters {A : ℤ → spectrum} (f : Π(s : ℤ), A s →ₛ A (s - 1))
 
---  protected definition I [constructor] : Set := gℤ ×g gℤ
   local abbreviation I [constructor] := Z2
 
   definition D_sequence : graded_module rℤ I :=
@@ -778,16 +782,18 @@ namespace spectrum
   λv, LeftModule_int_of_AbGroup (πₛ[v.1] (sfiber (f (v.2))))
 
   include f
+
   definition i_sequence : D_sequence →gm D_sequence :=
   begin
-    fapply graded_hom.mk, exact (prod_equiv_prod erfl (add_right_action (- 1))),
+    fapply graded_hom.mk, exact (prod_equiv_prod erfl (add_right_action (- (1 : ℤ)))),
+    { intro i, exact pair_eq !add_zero⁻¹ idp },
     intro v,
     apply lm_hom_int.mk, esimp,
-    exact πₛ→[v.1] (f v.2)
+    rexact πₛ→[v.1] (f v.2)
   end
 
   definition deg_j_seq_inv [constructor] : I ≃ I :=
-  prod_equiv_prod (add_right_action 1) (add_right_action (- 1))
+  prod_equiv_prod (add_right_action (1 : ℤ)) (add_right_action (- (1 : ℤ)))
 
   definition fn_j_sequence [unfold 3] (x : I) :
     D_sequence (deg_j_seq_inv x) →lm E_sequence x :=
@@ -798,11 +804,11 @@ namespace spectrum
   end
 
   definition j_sequence : D_sequence →gm E_sequence :=
-  graded_hom.mk_out deg_j_seq_inv⁻¹ᵉ fn_j_sequence
+  graded_hom.mk_out deg_j_seq_inv⁻¹ᵉ (λi, idp) fn_j_sequence
 
   definition k_sequence : E_sequence →gm D_sequence :=
   begin
-    fapply graded_hom.mk erfl,
+    fapply graded_hom.mk erfl deg_eq_id,
     intro v, induction v with n s,
     apply lm_hom_int.mk, esimp,
     exact πₛ→[n] (spoint (f s))
@@ -816,10 +822,10 @@ namespace spectrum
     intro y, induction x with n s, induction y with m t,
     refine equiv_rect !pair_eq_pair_equiv⁻¹ᵉ _ _,
     intro pq, esimp at pq, induction pq with p q,
-    revert t q, refine eq.rec_equiv (add_right_action (- 1)) _,
+    revert t q, refine eq.rec_equiv (add_right_action (-(1 : ℤ))) _,
     induction p using eq.rec_symm,
     apply is_exact_homotopy homotopy.rfl,
-    { symmetry, exact graded_hom_mk_out_destruct deg_j_seq_inv⁻¹ᵉ fn_j_sequence },
+    { symmetry, exact graded_hom_mk_out_destruct deg_j_seq_inv⁻¹ᵉ (λi, idp) fn_j_sequence },
     rexact is_exact_of_is_exact_at (is_exact_LES_of_shomotopy_groups (f s) (m, 2)),
   end
 
@@ -829,7 +835,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, exact graded_hom_mk_out_destruct deg_j_seq_inv⁻¹ᵉ fn_j_sequence },
+    { symmetry, exact graded_hom_mk_out_destruct deg_j_seq_inv⁻¹ᵉ (λi, idp) fn_j_sequence },
     { reflexivity },
     rexact is_exact_of_is_exact_at (is_exact_LES_of_shomotopy_groups (f s) (n, 1)),
   end
@@ -846,7 +852,7 @@ namespace spectrum
 
   open int
   parameters (ub : ℤ → ℤ) (lb : ℤ → ℤ)
-    (Aub : Π(s n : ℤ), s ≥ ub n + 1 → is_equiv (πₛ→[n] (f s)))
+    (Aub : Π(s n : ℤ), s ≥ ub n + (1 : ℤ) → is_equiv (πₛ→[n] (f s)))
     (Alb : Π(s n : ℤ), s ≤ lb n → is_contr (πₛ[n] (A s)))
 
   definition B : I → ℕ
@@ -856,7 +862,7 @@ namespace spectrum
   | (n, s) := max0 (ub n - s)
 
   definition B'' : I → ℕ
-  | (n, s) := max0 (max (ub n + 1 - s) (ub (n+1) + 1 - s))
+  | (n, s) := max0 (max (ub n + (1 : ℤ) - s) (ub (n+(1 : ℤ)) + (1 : ℤ) - s))
 
   lemma iterate_deg_i (n s : ℤ) (m : ℕ) : (deg i_sequence)^[m] (n, s) = (n, s - m) :=
   begin
@@ -904,11 +910,11 @@ namespace spectrum
 
   definition is_bounded_sequence [constructor] : is_bounded exact_couple_sequence :=
   is_bounded.mk B B' B'' Dub Dlb Elb
-    (by intro x; reflexivity)
-    begin
-      intro x, induction x with n s, apply pair_eq, esimp, esimp, esimp [j_sequence, i_sequence],
-      refine !add.assoc ⬝ ap (add s) !add.comm ⬝ !add.assoc⁻¹,
-    end
+    -- (by intro x; reflexivity)
+    -- begin
+    --   intro x, induction x with n s, apply pair_eq, esimp, esimp, esimp [j_sequence, i_sequence],
+    --   refine !add.assoc ⬝ ap (add s) !add.comm ⬝ !add.assoc⁻¹,
+    -- end
 
   definition converges_to_sequence : (λn s, πₛ[n] (sfiber (f s))) ⟹ᵍ (λn, πₛ[n] (A (ub n))) :=
   begin
@@ -919,8 +925,8 @@ namespace spectrum
     { intro n, change max0 (ub n - ub n) = 0, exact ap max0 (sub_self (ub n)) },
     { intro ns, reflexivity },
     { intro n, reflexivity },
-    { intro r, exact - 1 },
-    { intro r, exact r + 1 },
+    { intro r, exact - (1 : ℤ) },
+    { intro r, exact r + (1 : ℤ) },
     { intro r n s, refine !convergence_theorem.deg_d ⬝ _,
       refine ap (deg j_sequence) !iterate_deg_i_inv ⬝ _,
       exact prod_eq idp (!add.assoc ⬝ ap (λx, s + (r + x)) !neg_neg) },
@@ -933,7 +939,7 @@ namespace spectrum
 
 -- print axioms is_bounded_sequence
 
--- I think it depends on univalence in an essential way. The reason is that the long exact sequence
+-- It depends on univalence in an essential way. The reason is that the long exact sequence
 -- of homotopy groups already depends on univalence. Namely, in that proof we need to show that if f
 -- : A → B and g : B → C are exact at B, then ∥A∥₀ → ∥B∥₀ → ∥C∥₀ is exact at ∥B∥₀. For this we need
 -- that the equality |b|₀ = |b'|₀ is equivalent to ∥b = b'∥₋₁, which requires univalence.
diff --git a/cohomology/projective_space.hlean b/cohomology/projective_space.hlean
index 14b691f..8521394 100644
--- a/cohomology/projective_space.hlean
+++ b/cohomology/projective_space.hlean
@@ -62,7 +62,7 @@ namespace temp
   transport (is_contr ∘ E∞)
     begin
       induction m with m q, reflexivity, refine ap (deg (exact_couple.i X)) q ⬝ _,
-      exact prod_eq idp (neg_add m 1)⁻¹
+      exact prod_eq idp (neg_add m (1 : ℤ))⁻¹ᵖ
     end
     (fEinfd n m p)
 
@@ -103,20 +103,20 @@ namespace temp
       unreduced_ordinary_cohomology_isomorphism_right _ uH0_circle _,
   end
 
-  definition Ex1 (n : ℕ) : AddGroup_of_AddAbGroup (E (-(n+1),- 1)) ≃g uH^n[K agℤ 2] :=
+  definition Ex1 (n : ℕ) : AddGroup_of_AddAbGroup (E (-(n+(1 : ℤ)),- (1 : ℤ))) ≃g uH^n[K agℤ 2] :=
   begin
-    refine group_isomorphism_of_lm_isomorphism_int (converges_to.e fserre (-(n+1),- 1)) ⬝g _,
+    refine group_isomorphism_of_lm_isomorphism_int (converges_to.e fserre (-(n+(1 : ℤ)),- (1 : ℤ))) ⬝g _,
     refine cohomology_change_int _ _ (ap neg _ ⬝ !neg_neg) ⬝g
       unreduced_ordinary_cohomology_isomorphism_right _ !uH1_circle _,
-    exact ap (λx, x - - 1) !neg_add ⬝ !add_sub_cancel
+    exact ap (λx, x - - (1 : ℤ)) !neg_add ⬝ !add_sub_cancel
   end
 
   definition uH0 : uH^0[K agℤ 2] ≃g gℤ :=
   (Ex0 0)⁻¹ᵍ ⬝g group_isomorphism_of_lm_isomorphism_int fE00
 
-  definition fE10 : is_contr (E (- 1,0)) :=
+  definition fE10 : is_contr (E (- (1 : ℤ),0)) :=
   begin
-    refine @(is_trunc_equiv_closed _ _) (fEinf (- 1) 0 dec_star),
+    refine @(is_trunc_equiv_closed _ _) (fEinf (- (1 : ℤ)) 0 dec_star),
     apply equiv_of_isomorphism,
     refine Einf_isomorphism fserre 0 _ _,
     intro r H, exact sorry, exact sorry --apply is_contr_fD2, change (- 1) - (- 1) >[ℤ] (- 0) - (r + 1),
diff --git a/homotopy/EM.hlean b/homotopy/EM.hlean
index fe19189..d38a5c1 100644
--- a/homotopy/EM.hlean
+++ b/homotopy/EM.hlean
@@ -403,20 +403,27 @@ namespace EM
   EM_homomorphism_gloop (deloop X) n
     ((gloopn_succ_in' n (deloop X))⁻¹ᵍ⁸ ∘∞g Ωg'→[n] (deloop_isomorphism X)⁻¹ᵍ⁸ ∘∞g e)
 
-  definition is_mul_hom_EM_functor [constructor] (G H : AbGroup) (n : ℕ) :
-    is_mul_hom (λ(φ : G →gg H), EM_functor φ n) :=
-  begin
-    intro φ ψ,
-    apply eq_of_phomotopy,
-    exact sorry
-    -- exact sorry, exact sorry, exact sorry
---    refine idpath (φ 0 * ψ 0) ⬝ _,
-  end
+--   definition is_mul_hom_EM_functor [constructor] (G H : AbGroup) (n : ℕ) :
+--     is_mul_hom (λ(φ : G →gg H), EM_functor φ n) :=
+--   begin
+--     intro φ ψ,
+--     apply eq_of_phomotopy,
+--     exact sorry
+--     -- exact sorry, exact sorry, exact sorry
+-- --    refine idpath (φ 0 * ψ 0) ⬝ _,
+--   end
 
   /- an enriched homomorphism -/
   definition EM_ehomomorphism [constructor] (G H : AbGroup) (n : ℕ) :
     InfGroup_of_Group (G →gg H) →∞g InfGroup_of_deloopable (EM G n →** EM H n) :=
-  inf_homomorphism.mk (λφ, EM_functor φ n) (is_mul_hom_EM_functor G H n)
+  inf_homomorphism.mk (λφ, EM_functor φ n)
+    begin
+      intro φ ψ,
+      apply eq_of_phomotopy,
+      exact sorry
+      -- exact sorry, exact sorry, exact sorry
+  --    refine idpath (φ 0 * ψ 0) ⬝ _,
+    end
 
   -- definition EM_homomorphism [unfold 8] {G : AbGroup} {X : Type*} (Y : Type*) (e : Ω Y ≃* X) (n : ℕ)
   --   (e : AbInfGroup_of_AbGroup G →∞g Ωg[succ n] X) [H : is_trunc n X] : gEM G n →∞g X :=