diff --git a/algebra/exactness.hlean b/algebra/exactness.hlean
index 1af74b2..9fdec90 100644
--- a/algebra/exactness.hlean
+++ b/algebra/exactness.hlean
@@ -219,6 +219,30 @@ begin
   { exact is_short_exact.ker_in_im H }
 end
 
+lemma is_equiv_left_of_is_short_exact {A B C : Group} {f : A →g B} {g : B →g C}
+  (H : is_short_exact f g) (HC : is_contr C) : is_equiv f :=
+begin
+  apply is_equiv_of_is_surjective_of_is_embedding,
+    exact is_short_exact.is_emb H,
+    apply is_surjective_of_is_exact_of_is_contr, exact is_exact_of_is_short_exact H
+end
+
+lemma is_equiv_right_of_is_short_exact {A B C : Group} {f : A →g B} {g : B →g C}
+  (H : is_short_exact f g) (HA : is_contr A) : is_equiv g :=
+begin
+  apply is_equiv_of_is_surjective_of_is_embedding,
+    apply is_embedding_of_is_exact_g, exact is_exact_of_is_short_exact H,
+    exact is_short_exact.is_surj H
+end
+
+definition is_contr_right_of_is_short_exact {A B : Type} {C : Type*} {f : A → B} {g : B → C}
+  (H : is_short_exact f g) (HB : is_contr B) (HC : is_set C) : is_contr C :=
+is_contr_of_is_surjective g (is_short_exact.is_surj H) HB HC
+
+definition is_contr_left_of_is_short_exact {A B : Type} {C : Type*} {f : A → B} {g : B → C}
+  (H : is_short_exact f g) (HB : is_contr B) (a₀ : A) : is_contr A :=
+is_contr_of_is_embedding f (is_short_exact.is_emb H) _ a₀
+
 /- TODO: move and remove other versions -/
 
   definition is_surjective_qg_map {A : Group} (N : property A) [is_normal_subgroup A N] :
diff --git a/algebra/graded.hlean b/algebra/graded.hlean
index c7a9194..d4f3f85 100644
--- a/algebra/graded.hlean
+++ b/algebra/graded.hlean
@@ -196,6 +196,10 @@ graded_hom.mk erfl (λ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₂) :
+  (λ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))
+
 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₂)
 
@@ -647,5 +651,9 @@ 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') :
+  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)
+
 
 end left_module
diff --git a/algebra/left_module.hlean b/algebra/left_module.hlean
index 6dfe619..cdc293f 100644
--- a/algebra/left_module.hlean
+++ b/algebra/left_module.hlean
@@ -195,6 +195,11 @@ definition LeftModule_of_AddAbGroup {R : Ring} (G : AddAbGroup) (smul : R → G
   (h1 h2 h3 h4) : LeftModule R :=
 LeftModule.mk G (left_module_of_ab_group smul h1 h2 h3 h4)
 
+open unit
+definition trivial_LeftModule [constructor] (R : Ring) : LeftModule R :=
+LeftModule_of_AddAbGroup trivial_ab_group (λr u, star)
+  (λr u₁ u₂, idp) (λr₁ r₂ u, idp) (λr₁ r₂ u, idp) unit.eta
+
 section
   variables {R : Ring} {M M₁ M₂ M₃ : LeftModule R}
 
@@ -389,6 +394,15 @@ end
     (φ : M₁ →a M₂) (h : Π(r : R) g, φ (r • g) = r • φ g) : M₁ →lm M₂ :=
   homomorphism.mk' φ (group.to_respect_add φ) h
 
+  definition group_isomorphism_of_lm_isomorphism [constructor] {M₁ M₂ : LeftModule R}
+    (φ : M₁ ≃lm M₂) : AddGroup_of_AddAbGroup M₁ ≃g AddGroup_of_AddAbGroup M₂ :=
+  group.isomorphism.mk (group_homomorphism_of_lm_homomorphism φ) (isomorphism.is_equiv_to_hom φ)
+
+  definition lm_isomorphism_of_group_isomorphism [constructor] {M₁ M₂ : LeftModule R}
+    (φ : AddGroup_of_AddAbGroup M₁ ≃g AddGroup_of_AddAbGroup M₂)
+    (h : Π(r : R) g, φ (r • g) = r • φ g) : M₁ ≃lm M₂ :=
+  isomorphism.mk (lm_homomorphism_of_group_homomorphism φ h) (group.isomorphism.is_equiv_to_hom φ)
+
   section
   local attribute pSet_of_LeftModule [coercion]
   definition is_exact_mod (f : M₁ →lm M₂) (f' : M₂ →lm M₃) : Type :=
@@ -425,6 +439,34 @@ end
     (HA : is_contr A) (HC : is_contr C) : is_contr B :=
   is_contr_middle_of_is_exact (is_exact_of_is_short_exact (short_exact_mod.h H))
 
+  definition is_contr_right_of_short_exact_mod {A B C : LeftModule R} (H : short_exact_mod A B C)
+    (HB : is_contr B) : is_contr C :=
+  is_contr_right_of_is_short_exact (short_exact_mod.h H) _ _
+
+  definition is_contr_left_of_short_exact_mod {A B C : LeftModule R} (H : short_exact_mod A B C)
+    (HB : is_contr B) : is_contr A :=
+  is_contr_left_of_is_short_exact (short_exact_mod.h H) _ pt
+
+  definition isomorphism_of_is_contr_left {A B C : LeftModule R} (H : short_exact_mod A B C)
+    (HA : is_contr A) : B ≃lm C :=
+  isomorphism.mk (short_exact_mod.g H)
+    begin
+      apply @is_equiv_right_of_is_short_exact _ _ _
+        (group_homomorphism_of_lm_homomorphism (short_exact_mod.f H))
+        (group_homomorphism_of_lm_homomorphism (short_exact_mod.g H)),
+      rexact short_exact_mod.h H, exact HA,
+    end
+
+  definition isomorphism_of_is_contr_right {A B C : LeftModule R} (H : short_exact_mod A B C)
+    (HC : is_contr C) : A ≃lm B :=
+  isomorphism.mk (short_exact_mod.f H)
+    begin
+      apply @is_equiv_left_of_is_short_exact _ _ _
+        (group_homomorphism_of_lm_homomorphism (short_exact_mod.f H))
+        (group_homomorphism_of_lm_homomorphism (short_exact_mod.g H)),
+      rexact short_exact_mod.h H, exact HC,
+    end
+
   end
 
   end
@@ -446,6 +488,11 @@ lm_homomorphism_of_group_homomorphism φ (to_respect_imul φ)
 definition lm_iso_int.mk [constructor] {A B : AbGroup} (φ : A ≃g B) :
   LeftModule_int_of_AbGroup A ≃lm LeftModule_int_of_AbGroup B :=
 isomorphism.mk (lm_hom_int.mk φ) (group.isomorphism.is_equiv_to_hom φ)
+
+definition group_isomorphism_of_lm_isomorphism_int [constructor] {A B : AbGroup}
+  (φ : LeftModule_int_of_AbGroup A ≃lm LeftModule_int_of_AbGroup B) : A ≃g B :=
+group_isomorphism_of_lm_isomorphism φ
+
 end int
 
 end left_module
diff --git a/algebra/spectral_sequence.hlean b/algebra/spectral_sequence.hlean
index 4f7152b..5240c7d 100644
--- a/algebra/spectral_sequence.hlean
+++ b/algebra/spectral_sequence.hlean
@@ -7,12 +7,70 @@
 
 import .graded ..spectrum.basic .product_group
 
-open algebra is_trunc left_module is_equiv equiv eq function nat sigma sigma.ops set_quotient
+open algebra is_trunc left_module is_equiv equiv eq function nat sigma set_quotient
 
 /- exact couples -/
 
 namespace left_module
 
+  section
+  /- move to left_module -/
+  structure is_built_from.{u v w} {R : Ring} (D : LeftModule.{u v} R)
+      (E : ℕ → LeftModule.{u w} R) : Type.{max u (v+1) w} :=
+    (part : ℕ → LeftModule.{u v} R)
+    (ses : Πn, short_exact_mod (E n) (part n) (part (n+1)))
+    (e0 : part 0 ≃lm D)
+    (n₀ : ℕ)
+    (HD' : Π(s : ℕ), n₀ ≤ s → is_contr (part s))
+
+  open is_built_from
+  universe variables u v w
+  variables {R : Ring.{u}} {D D' : LeftModule.{u v} R} {E E' : ℕ → LeftModule.{u w} R}
+
+  definition is_built_from_shift (H : is_built_from D E) :
+    is_built_from (part H 1) (λn, E (n+1)) :=
+  is_built_from.mk (λn, part H (n+1)) (λn, ses H (n+1)) isomorphism.rfl (pred (n₀ H))
+    (λs Hle, HD' H _ (le_succ_of_pred_le Hle))
+
+  definition isomorphism_of_is_contr_part (H : is_built_from D E) (n : ℕ) (HE : is_contr (E n)) :
+    part H n ≃lm part H (n+1) :=
+  isomorphism_of_is_contr_left (ses H n) HE
+
+  definition is_contr_submodules (H : is_built_from D E) (HD : is_contr D) (n : ℕ) :
+    is_contr (part H n) :=
+  begin
+    induction n with n IH,
+    { exact is_trunc_equiv_closed_rev -2 (equiv_of_isomorphism (e0 H)) },
+    { exact is_contr_right_of_short_exact_mod (ses H n) IH }
+  end
+
+  definition is_contr_quotients (H : is_built_from D E) (HD : is_contr D) (n : ℕ) :
+    is_contr (E n) :=
+  begin
+    apply is_contr_left_of_short_exact_mod (ses H n),
+    exact is_contr_submodules H HD n
+  end
+
+  definition is_contr_total (H : is_built_from D E) (HE : Πn, is_contr (E n)) : is_contr D :=
+  have is_contr (part H 0), from
+  nat.rec_down (λn, is_contr (part H n)) _ (HD' H _ !le.refl)
+    (λn H2, is_contr_middle_of_short_exact_mod (ses H n) (HE n) H2),
+  is_contr_equiv_closed (equiv_of_isomorphism (e0 H))
+
+  definition is_built_from_isomorphism (e : D ≃lm D') (f : Πn, E n ≃lm E' n)
+    (H : is_built_from D E) : is_built_from D' E' :=
+  ⦃is_built_from, H, e0 := e0 H ⬝lm e,
+    ses := λn, short_exact_mod_isomorphism (f n)⁻¹ˡᵐ isomorphism.rfl isomorphism.rfl (ses H n)⦄
+
+  definition is_built_from_isomorphism_left (e : D ≃lm D') (H : is_built_from D E) :
+    is_built_from D' E :=
+  ⦃is_built_from, H, e0 := e0 H ⬝lm e⦄
+
+  definition isomorphism_zero_of_is_built_from (H : is_built_from D E) (p : n₀ H = 1) : E 0 ≃lm D :=
+  isomorphism_of_is_contr_right (ses H 0) (HD' H 1 (le_of_eq p)) ⬝lm e0 H
+
+  end
+
   structure exact_couple (R : Ring) (I : Set) : Type :=
     (D E : graded_module R I)
     (i : D →gm D) (j : D →gm E) (k : E →gm D)
@@ -22,6 +80,13 @@ namespace left_module
 
   open exact_couple
 
+  definition exact_couple_reindex [constructor] {R : Ring} {I J : Set} (e : J ≃ 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)⦄
+
   namespace derived_couple
   section
 
@@ -45,6 +110,10 @@ namespace left_module
   definition is_contr_D' {x : I} (H : is_contr (D x)) : is_contr (D' x) :=
   !is_contr_image_module
 
+  definition E'_isomorphism {x : I} (H1 : is_contr (E ((deg d)⁻¹ᵉ x)))
+    (H2 : is_contr (E (deg d x))) : E' x ≃lm E x :=
+  @(homology_isomorphism _ _) H1 H2
+
   definition i' : D' →gm D' :=
   graded_image_lift i ∘gm  graded_submodule_incl (λx, image (i ← x))
 
@@ -114,9 +183,10 @@ namespace left_module
   end
 
   definition k' : E' →gm D' :=
-  @graded_quotient_elim _ _ _ _ _ _ (graded_submodule_functor k k_lemma1)
+  @graded_quotient_elim _ _ _ _ _ _ k₂
                        (by intro x m h; cases m with [m1, m2]; exact k_lemma2 m1 m2 h)
 
+  open sigma.ops
   definition i'_eq ⦃x : I⦄ (m : D x) (h : image (i ← x) m) : (i' x ⟨m, h⟩).1 = i x m :=
   by reflexivity
 
@@ -234,18 +304,34 @@ namespace left_module
   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) },
-    { intro x y z s p q h, induction p, induction q,
+    { 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 },
+      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 }
   end
 
+  open is_bounded
+  definition is_bounded_reindex [constructor] {R : Ring} {I J : Set} (e : J ≃ 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 _ },
+    { 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 _ },
+    { 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 _)⁻¹) }
+  end
+
   namespace convergence_theorem
   section
 
-  open is_bounded
   parameters {R : Ring} {I : Set} (X : exact_couple R I) (HH : is_bounded X)
 
   local abbreviation B := B HH
@@ -256,25 +342,7 @@ namespace left_module
   local abbreviation deg_ik_commute := deg_ik_commute HH
   local abbreviation deg_ij_commute := deg_ij_commute HH
 
-  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
-
-  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)
-
-  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) :
-    is_contr (E X y) :=
-  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)
-  end
-
-  -- we start counting pages at 0
+  /- We start counting pages at 0, which corresponds to what is usually called the second page -/
   definition page (r : ℕ) : exact_couple R I :=
   iterate derived_couple r X
 
@@ -324,6 +392,45 @@ namespace left_module
     (deg (d (page r)))⁻¹ ~ (deg (k X))⁻¹ ∘ iterate (deg (i X)) r ∘ (deg (j X))⁻¹ :=
   compose2 (to_inv_homotopy_inv (deg_k r)) (deg_j_inv r)
 
+  definition E_isomorphism' {x : I} {r₁ r₂ : ℕ} (H : r₁ ≤ r₂)
+    (H1 : Π⦃r⦄, r₁ ≤ r → r < r₂ → is_contr (E X ((deg (d (page r)))⁻¹ᵉ x)))
+    (H2 : Π⦃r⦄, r₁ ≤ r → r < r₂ → is_contr (E X (deg (d (page r)) x))) :
+    E (page r₂) x ≃lm E (page r₁) x :=
+  begin
+    assert H2 : Π⦃r⦄, r₁ ≤ r → r ≤ r₂ → E (page r) x ≃lm E (page r₁) x,
+    { intro r Hr₁ Hr₂,
+      induction Hr₁ with r Hr₁ IH, reflexivity,
+      let Hr₂' := le_of_succ_le Hr₂,
+      exact E'_isomorphism (page r) (is_contr_E r _ (H1 Hr₁ Hr₂)) (is_contr_E r _ (H2 Hr₁ Hr₂))
+        ⬝lm IH Hr₂' },
+    exact H2 H (le.refl _)
+  end
+
+  definition E_isomorphism0' {x : I} {r : ℕ}
+    (H1 : Πr, is_contr (E X ((deg (d (page r)))⁻¹ᵉ x)))
+    (H2 : Πr, is_contr (E X (deg (d (page r)) x))) : E (page r) x ≃lm E X x :=
+  E_isomorphism' (zero_le r) _ _
+
+  parameter {X}
+
+  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
+
+  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)
+
+  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) :
+    is_contr (E X y) :=
+  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)
+  end
+
   definition B3 (x : I) : ℕ :=
   max (B (deg (j X) (deg (k X) x))) (B2 ((deg (k X))⁻¹ ((deg (j X))⁻¹ x)))
 
@@ -344,12 +451,6 @@ 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 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,
-      -- exact sorry
     { change is_surjective (i' (page r) ↘ p),
       apply is_surjective_i', intro z' q',
       refine IH _ _ _ _ (le.trans H (le_of_eq (succ_add s r)⁻¹)) _ _,
@@ -379,6 +480,22 @@ namespace left_module
   definition Dinfstable {x y : I} {r : ℕ} (Hr : B' y ≤ r) (p : x = y) : Dinf y ≃lm D (page r) x :=
   by symmetry; induction p; induction Hr with r Hr IH; reflexivity; exact Dstable Hr ⬝lm IH
 
+  definition Einf_isomorphism' {x : I} (r₁ : ℕ)
+    (H1 : Π⦃r⦄, r₁ ≤ r → is_contr (E X ((deg (d (page r)))⁻¹ᵉ x)))
+    (H2 : Π⦃r⦄, r₁ ≤ r → is_contr (E X (deg (d (page r)) x))) :
+    Einf x ≃lm E (page r₁) x :=
+  begin
+    cases le.total r₁ (B3 x) with Hr Hr,
+    exact E_isomorphism' Hr (λr Hr₁ Hr₂, H1 Hr₁) (λr Hr₁ Hr₂, H2 Hr₁),
+    exact Einfstable Hr idp
+  end
+
+  definition Einf_isomorphism0' {x : I}
+    (H1 : Π⦃r⦄, is_contr (E X ((deg (d (page r)))⁻¹ᵉ x)))
+    (H2 : Π⦃r⦄, is_contr (E X (deg (d (page r)) x))) :
+    Einf x ≃lm E X x :=
+  E_isomorphism0' _ _
+
   parameters (x : I)
 
   definition r (n : ℕ) : ℕ :=
@@ -426,7 +543,6 @@ 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
@@ -453,26 +569,40 @@ namespace left_module
     { reflexivity }
   end
 
+  /- the convergence theorem is the following result -/
+  definition is_built_from_infpage (bound_zero : B' (deg (k X) x) = 0) :
+    is_built_from (D X (deg (k X) x)) Einfdiag :=
+  is_built_from.mk Dinfdiag short_exact_mod_infpage (Dinfdiag0 bound_zero) (B (deg (k X) x))
+    (λs, Dinfdiag_stable)
+
   end
   end convergence_theorem
 
-  -- open convergence_theorem
-  -- print axioms short_exact_mod_infpage
-  -- print axioms Dinfdiag0
-  -- print axioms Dinfdiag_stable
-
   open int group prod convergence_theorem prod.ops
 
   definition Z2 [constructor] : Set := gℤ ×g 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)} :=
-    (X : exact_couple.{u 0 v w} R Z2)
+    (X : exact_couple.{u 0 w v} R Z2)
     (HH : is_bounded X)
     (s₀ : gℤ → gℤ)
-    (p : Π(n : gℤ), is_bounded.B' HH (deg (k X) (n, s₀ n)) = 0)
-    (e : Π(x : gℤ ×g gℤ), exact_couple.E X x ≃lm E' x.1 x.2)
+    (HB : Π(n : gℤ), 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))
+
+  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)} :=
+    (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)))
 
   infix ` ⟹ `:25 := converges_to
 
@@ -488,15 +618,43 @@ namespace left_module
   local abbreviation i := i X
   local abbreviation HH := HH c
   local abbreviation s₀ := s₀ c
-  local abbreviation Dinfdiag (n : gℤ) (k : ℕ) := Dinfdiag X HH (n, s₀ n) k
-  local abbreviation Einfdiag (n : gℤ) (k : ℕ) := Einfdiag X HH (n, s₀ n) k
+  local abbreviation Dinfdiag (n : gℤ) (k : ℕ) := Dinfdiag HH (n, s₀ n) k
+  local abbreviation Einfdiag (n : gℤ) (k : ℕ) := Einfdiag HH (n, s₀ n) k
+
+  definition deg_d_inv_eq (r : ℕ) (n s : gℤ) :
+    (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ℤ}
     (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₀ (p c)
+  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)) :
+    (λ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ℤ}
+    (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 :=
+  converges_to.mk (exact_couple_reindex (equiv_neg ×≃ equiv_neg) X) (is_bounded_reindex _ HH)
+    (λn, -s₀ (-n))
+    (λn, ap (B' HH) (begin esimp, 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 is_built_from_of_converges_to (n : ℤ) : is_built_from (Dinf n) (Einfdiag n) :=
+  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)) :
     is_contr (Dinf n) :=
@@ -509,15 +667,41 @@ namespace left_module
       { exact is_bounded.B HH (deg (k X) (n, s₀ n)) },
       { apply Dinfdiag_stable, reflexivity },
       { intro l H,
-        exact is_contr_middle_of_short_exact_mod (short_exact_mod_infpage X HH (n, s₀ n) l)
+        exact is_contr_middle_of_short_exact_mod (short_exact_mod_infpage HH (n, s₀ n) l)
                 (H2 l) H }},
     refine @is_trunc_equiv_closed _ _ _ _ H3,
-    exact equiv_of_isomorphism (Dinfdiag0 X HH (n, s₀ n) (p c n) ⬝lm f c n)
+    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) :=
   is_contr_converges_to_precise n (λn s, !H)
 
+  definition E_isomorphism {r₁ r₂ : ℕ} {n s : gℤ} (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ℤ}
+    (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ℤ}
+    (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ℤ}
+    (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 :=
+  E_isomorphism0 _ _
+
   end
 
   variables {E' : gℤ → gℤ → AbGroup} {Dinf : gℤ → AbGroup} (c : E' ⟹ᵍ Dinf)
@@ -734,7 +918,12 @@ namespace spectrum
     { intro n, exact ub },
     { intro n, change max0 (ub - ub) = 0, exact ap max0 (sub_self ub) },
     { intro ns, reflexivity },
-    { intro n, reflexivity }
+    { intro n, reflexivity },
+    { 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) },
   end
 
   end
diff --git a/algebra/submodule.hlean b/algebra/submodule.hlean
index 980c375..279feed 100644
--- a/algebra/submodule.hlean
+++ b/algebra/submodule.hlean
@@ -209,6 +209,7 @@ begin
   intro m, exact to_one_smul m
 end
 
+variable (S)
 definition quotient_module (S : property M) [is_submodule M S] : LeftModule R :=
 LeftModule_of_AddAbGroup (quotient_module' S) (quotient_module_smul S)
   (λr, homomorphism.addstruct (quotient_module_smul S r))
@@ -216,7 +217,7 @@ LeftModule_of_AddAbGroup (quotient_module' S) (quotient_module_smul S)
   quotient_module_mul_smul
   quotient_module_one_smul
 
-definition quotient_map [constructor] (S : property M) [is_submodule M S] : M →lm quotient_module S :=
+definition quotient_map [constructor] : 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 :=
@@ -225,6 +226,7 @@ definition quotient_map_eq_zero (m : M) (H : S m) : quotient_map S m = 0 :=
 definition rel_of_quotient_map_eq_zero (m : M) (H : quotient_map S m = 0) : S m :=
 @rel_of_qg_map_eq_one _ _ (is_normal_subgroup_ab _) m H
 
+variable {S}
 definition quotient_elim [constructor] (φ : M →lm M₂) (H : Π⦃m⦄, m ∈ S → φ m = 0) :
   quotient_module S →lm M₂ :=
 lm_homomorphism_of_group_homomorphism
@@ -244,6 +246,10 @@ definition is_contr_quotient_module [instance] (S : property M) [is_submodule M
   is_contr (quotient_module S) :=
 is_contr_of_inhabited_prop 0
 
+definition rel_of_is_contr_quotient_module (S : property M) [is_submodule M S]
+  (H : is_contr (quotient_module S)) (m : M) : S m :=
+rel_of_quotient_map_eq_zero S m (@eq_of_is_contr _ H _ _)
+
 definition quotient_module_isomorphism [constructor] (S : property M) [is_submodule M S] (h : Π⦃m⦄, S m → m = 0) :
   quotient_module S ≃lm M :=
 (isomorphism.mk (quotient_map S) (is_equiv_ab_qg_map S h))⁻¹ˡᵐ
@@ -420,6 +426,32 @@ definition homology_isomorphism [constructor] (ψ : M₂ →lm M₃) (φ : M₁
 (quotient_module_isomorphism (homology_quotient_property ψ φ)
   (eq_zero_of_mem_property_submodule_trivial (image_trivial _))) ⬝lm (kernel_module_isomorphism ψ)
 
+definition ker_in_im_of_is_contr_homology (ψ : M₂ →lm M₃) {φ : M₁ →lm M₂}
+  (H₁ : is_contr (homology ψ φ)) {m : M₂} (p : ψ m = 0) : image φ m :=
+rel_of_is_contr_quotient_module _ H₁ ⟨m, p⟩
+
+definition is_embedding_of_is_contr_homology_of_constant {ψ : M₂ →lm M₃} (φ : M₁ →lm M₂)
+  (H₁ : is_contr (homology ψ φ)) (H₂ : Πm, φ m = 0) : is_embedding ψ :=
+begin
+  apply to_is_embedding_homomorphism (group_homomorphism_of_lm_homomorphism ψ),
+  intro m p, note H := rel_of_is_contr_quotient_module _ H₁ ⟨m, p⟩,
+  induction H with n q,
+  exact q⁻¹ ⬝ H₂ n
+end
+
+definition is_embedding_of_is_contr_homology_of_is_contr {ψ : M₂ →lm M₃} (φ : M₁ →lm M₂)
+  (H₁ : is_contr (homology ψ φ)) (H₂ : is_contr M₁) : is_embedding ψ :=
+is_embedding_of_is_contr_homology_of_constant φ H₁
+  (λm, ap φ (@eq_of_is_contr _ H₂ _ _) ⬝ respect_zero φ)
+
+definition is_surjective_of_is_contr_homology_of_constant (ψ : M₂ →lm M₃) {φ : M₁ →lm M₂}
+  (H₁ : is_contr (homology ψ φ)) (H₂ : Πm, ψ m = 0) : is_surjective φ :=
+λm, ker_in_im_of_is_contr_homology ψ H₁ (H₂ m)
+
+definition is_surjective_of_is_contr_homology_of_is_contr (ψ : M₂ →lm M₃) {φ : M₁ →lm M₂}
+  (H₁ : is_contr (homology ψ φ)) (H₂ : is_contr M₃) : is_surjective φ :=
+is_surjective_of_is_contr_homology_of_constant ψ H₁ (λm, @eq_of_is_contr _ H₂ _ _)
+
 -- remove:
 
 -- definition homology.rec (P : homology ψ φ → Type)
diff --git a/cohomology/basic.hlean b/cohomology/basic.hlean
index 1c4a2da..ec6bdbd 100644
--- a/cohomology/basic.hlean
+++ b/cohomology/basic.hlean
@@ -63,6 +63,7 @@ notation `upH^` n `[`:0 binders `, ` r:(scoped Y, unreduced_parametrized_cohomol
 notation `uopH^` n `[`:0 binders `, ` r:(scoped G, unreduced_ordinary_parametrized_cohomology G n) `]`:0 := r
 
 /- an alternate definition of cohomology -/
+
 definition parametrized_cohomology_isomorphism_shomotopy_group_spi {X : Type*} (Y : X → spectrum)
   {n m : ℤ} (p : -m = n) : pH^n[(x : X), Y x] ≃g πₛ[m] (spi X Y) :=
 begin
@@ -146,6 +147,14 @@ definition unreduced_cohomology_isomorphism_right (X : Type) {Y Y' : spectrum} (
   (n : ℤ) : uH^n[X, Y] ≃g uH^n[X, Y'] :=
 cohomology_isomorphism_right X₊ e n
 
+definition unreduced_ordinary_cohomology_isomorphism {X X' : Type} (f : X' ≃ X) (G : AbGroup)
+  (n : ℤ) : uoH^n[X, G] ≃g uoH^n[X', G] :=
+unreduced_cohomology_isomorphism f (EM_spectrum G) n
+
+definition unreduced_ordinary_cohomology_isomorphism_right (X : Type) {G G' : AbGroup}
+  (e : G ≃g G') (n : ℤ) : uoH^n[X, G] ≃g uoH^n[X, G'] :=
+unreduced_cohomology_isomorphism_right X (EM_spectrum_pequiv e) n
+
 definition parametrized_cohomology_isomorphism_right {X : Type*} {Y Y' : X → spectrum}
   (e : Πx n, Y x n ≃* Y' x n) (n : ℤ) : pH^n[(x : X), Y x] ≃g pH^n[(x : X), Y' x] :=
 parametrized_cohomology_isomorphism_shomotopy_group_spi Y !neg_neg ⬝g
@@ -201,6 +210,14 @@ begin
   refine is_conn.elim 0 _ _, reflexivity
 end
 
+definition cohomology_change_int (X : Type*) (Y : spectrum) {n n' : ℤ} (p : n = n') :
+  H^n[X, Y] ≃g H^n'[X, Y] :=
+isomorphism_of_eq (ap (λn, H^n[X, Y]) p)
+
+definition parametrized_cohomology_change_int (X : Type*) (Y : X → spectrum) {n n' : ℤ}
+  (p : n = n') : pH^n[(x : X), Y x] ≃g pH^n'[(x : X), Y x] :=
+isomorphism_of_eq (ap (λn, pH^n[(x : X), Y x]) p)
+
 /- suspension axiom -/
 
 definition cohomology_susp_2 (Y : spectrum) (n : ℤ) :
@@ -271,7 +288,7 @@ is_equiv_of_equiv_of_homotopy (additive_equiv H X Y n) begin intro f, induction
 /- dimension axiom for ordinary cohomology -/
 open is_conn trunc_index
 theorem EM_dimension' (G : AbGroup) (n : ℤ) (H : n ≠ 0) :
-  is_contr (ordinary_cohomology pbool G n) :=
+  is_contr (oH^n[pbool, G]) :=
 begin
   apply is_conn_equiv_closed 0 !pmap_pbool_equiv⁻¹ᵉ,
   apply is_conn_equiv_closed 0 !equiv_glue2⁻¹ᵉ,
@@ -290,10 +307,39 @@ theorem EM_dimension (G : AbGroup) (n : ℤ) (H : n ≠ 0) :
   (EM_dimension' G n H)
 
 open group algebra
-theorem ordinary_cohomology_pbool (G : AbGroup) : ordinary_cohomology pbool G 0 ≃g G :=
+theorem ordinary_cohomology_pbool (G : AbGroup) : oH^0[pbool, G] ≃g G :=
 sorry
 --isomorphism_of_equiv (trunc_equiv_trunc 0 (ppmap_pbool_pequiv _ ⬝e _)  ⬝e !trunc_equiv) sorry
 
+theorem is_contr_cohomology_of_is_contr_spectrum (n : ℤ) (X : Type*) (Y : spectrum) (H : is_contr (Y n)) :
+  is_contr (H^n[X, Y]) :=
+begin
+  apply is_trunc_trunc_of_is_trunc,
+  apply is_trunc_pmap,
+  apply is_trunc_equiv_closed_rev,
+  exact loop_pequiv_loop (loop_pequiv_loop (pequiv_ap Y (add.assoc n 1 1)⁻¹) ⬝e* (equiv_glue Y (n+1))⁻¹ᵉ*) ⬝e
+    (equiv_glue Y n)⁻¹ᵉ*
+end
+
+theorem is_contr_ordinary_cohomology (n : ℤ) (X : Type*) (G : AbGroup) (H : is_contr G) :
+  is_contr (oH^n[X, G]) :=
+begin
+  apply is_contr_cohomology_of_is_contr_spectrum,
+  exact is_contr_EM_spectrum _ _ H
+end
+
+theorem is_contr_unreduced_ordinary_cohomology (n : ℤ) (X : Type) (G : AbGroup) (H : is_contr G) :
+  is_contr (uoH^n[X, G]) :=
+is_contr_ordinary_cohomology _ _ _ H
+
+theorem is_contr_ordinary_cohomology_of_neg {n : ℤ} (X : Type*) (G : AbGroup) (H : n < 0) :
+  is_contr (oH^n[X, G]) :=
+begin
+  apply is_contr_cohomology_of_is_contr_spectrum,
+  cases n with n n, contradiction,
+  apply is_contr_EM_spectrum_neg
+end
+
 /- cohomology theory -/
 
 structure cohomology_theory.{u} : Type.{u+1} :=
diff --git a/cohomology/projective_space.hlean b/cohomology/projective_space.hlean
new file mode 100644
index 0000000..c2272f5
--- /dev/null
+++ b/cohomology/projective_space.hlean
@@ -0,0 +1,137 @@
+/- A computation of the cohomology groups of K(ℤ,2) using the Serre spectral sequence
+
+Author: Floris van Doorn-/
+
+import .serre
+
+open eq spectrum EM EM.ops int pointed cohomology left_module algebra group fiber is_equiv equiv
+     prod is_trunc function
+
+namespace temp
+
+  definition uH0_circle : uH^0[circle] ≃g gℤ :=
+  sorry
+
+  definition uH1_circle : uH^1[circle] ≃g gℤ :=
+  sorry
+
+  definition uH_circle_of_ge (n : ℤ) (h : n ≥ 2) : uH^n[circle] ≃g trivial_ab_group :=
+  sorry
+
+  definition f : unit → K agℤ 2 :=
+  λx, pt
+
+  definition fserre :
+    (λn s, uoH^-(n-s)[K agℤ 2, H^-s[circle₊]]) ⟹ᵍ (λn, H^-n[unit₊]) :=
+  proof
+  converges_to_g_isomorphism
+    (serre_convergence_map_of_is_conn pt f (EM_spectrum agℤ) 0
+      (is_strunc_EM_spectrum agℤ) (is_conn_EM agℤ 2))
+    begin
+      intro n s, apply unreduced_ordinary_cohomology_isomorphism_right,
+      apply unreduced_cohomology_isomorphism, symmetry,
+      refine !fiber_const_equiv ⬝e _,
+      refine loop_EM _ 1 ⬝e _,
+      exact EM_pequiv_circle
+    end
+    begin intro n, reflexivity end
+  qed
+
+  section
+  local notation `X`   := converges_to.X fserre
+  local notation `E∞`  := convergence_theorem.Einf (converges_to.HH fserre)
+  local notation `E∞d` := convergence_theorem.Einfdiag (converges_to.HH fserre)
+  local notation `E`   := exact_couple.E X
+
+  definition fbuilt (n : ℤ) :
+    is_built_from (LeftModule_int_of_AbGroup (H^-n[unit₊])) (E∞d (n, 0)) :=
+  is_built_from_of_converges_to fserre n
+
+  definition fEinf0 : E∞ (0, 0) ≃lm LeftModule_int_of_AbGroup agℤ :=
+  isomorphism_zero_of_is_built_from (fbuilt 0) (by reflexivity) ⬝lm
+  lm_iso_int.mk (cohomology_change_int _ _ neg_zero ⬝g
+    cohomology_isomorphism pbool_pequiv_add_point_unit _ _ ⬝g ordinary_cohomology_pbool _)
+
+  definition fEinfd (n : ℤ) (m : ℕ) (p : n ≠ 0) : is_contr (E∞d (n, 0) m) :=
+  have p' : -n ≠ 0, from λH, p (eq_zero_of_neg_eq_zero H),
+  is_contr_quotients (fbuilt n) (@(is_trunc_equiv_closed_rev -2
+    (group.equiv_of_isomorphism (cohomology_isomorphism pbool_pequiv_add_point_unit _ _)))
+    (EM_dimension' _ _ p')) _
+
+  definition fEinf (n : ℤ) (m : ℕ) (p : n ≠ 0) : is_contr (E∞ (n, -m)) :=
+  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)⁻¹
+    end
+    (fEinfd n m p)
+
+  definition is_contr_fD (n s : ℤ) (p : s > 0) : is_contr (E (n, s)) :=
+  have is_contr H^-s[circle₊], from
+  is_contr_ordinary_cohomology_of_neg _ _ (neg_neg_of_pos p),
+  have is_contr (uoH^-(n-s)[K agℤ 2, H^-s[circle₊]]), from
+  is_contr_unreduced_ordinary_cohomology _ _ _ _,
+  @(is_contr_equiv_closed (left_module.equiv_of_isomorphism (converges_to.e fserre (n, s))⁻¹ˡᵐ))
+    this
+
+  definition is_contr_fD2 (n s : ℤ) (p : n > s) : is_contr (E (n, s)) :=
+  have -(n-s) < 0, from neg_neg_of_pos (sub_pos_of_lt p),
+  @(is_contr_equiv_closed (left_module.equiv_of_isomorphism (converges_to.e fserre (n, s))⁻¹ˡᵐ))
+    (is_contr_ordinary_cohomology_of_neg _ _ this)
+
+  definition is_contr_fD3 (n s : ℤ) (p : s ≤ - 2) : is_contr (E (n, s)) :=
+  have -s ≥ 2, from sorry, --from neg_neg_of_pos (sub_pos_of_lt p),
+  @(is_contr_equiv_closed (group.equiv_of_isomorphism (unreduced_ordinary_cohomology_isomorphism_right _ (uH_circle_of_ge _ this)⁻¹ᵍ _) ⬝e
+    left_module.equiv_of_isomorphism (converges_to.e fserre (n, s))⁻¹ˡᵐ))
+    (is_contr_ordinary_cohomology _ _ _ !is_contr_unit)
+--(unreduced_ordinary_cohomology_isomorphism_right _ _ _)
+--(is_contr_ordinary_cohomology_of_neg _ _ this)
+--(is_contr_ordinary_cohomology_of_neg _ _ this)
+  definition fE00 : E (0,0) ≃lm LeftModule_int_of_AbGroup agℤ :=
+  begin
+    refine (Einf_isomorphism fserre 0 _ _)⁻¹ˡᵐ ⬝lm fEinf0,
+    intro r H, apply is_contr_fD2, exact sub_nat_lt 0 (r+1),
+    intro r H, apply is_contr_fD, change 0 + (r + 1) >[ℤ] 0,
+    apply of_nat_lt_of_nat_of_lt,
+    apply nat.zero_lt_succ,
+  end
+
+  definition Ex0 (n : ℕ) : AddGroup_of_AddAbGroup (E (-n,0)) ≃g uH^n[K agℤ 2] :=
+  begin
+    refine group_isomorphism_of_lm_isomorphism_int (converges_to.e fserre (-n,0)) ⬝g _,
+    refine cohomology_change_int _ _ (ap neg !sub_zero ⬝ !neg_neg) ⬝g
+      unreduced_ordinary_cohomology_isomorphism_right _ uH0_circle _,
+  end
+
+  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 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
+  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)) :=
+  begin
+    refine @(is_trunc_equiv_closed _ _) (fEinf (- 1) 0 dec_star),
+    apply equiv_of_isomorphism,
+    refine Einf_isomorphism fserre 0 _ _,
+    intro r H, --apply is_contr_fD2, change (- 1) - (- 1) >[ℤ] (- 0) - (r + 1),
+--    apply is_contr_fD, change (-0) - (r + 1) >[ℤ] 0,
+--exact sub_nat_lt 0 r,
+    -- intro r H, apply is_contr_fD, change 0 + (r + 1) >[ℤ] 0,
+    -- apply of_nat_lt_of_nat_of_lt,
+    -- apply nat.zero_lt_succ,
+  end
+
+  definition uH1 : is_contr (uH^1[K agℤ 2]) :=
+  begin
+    refine @(is_trunc_equiv_closed -2 (group.equiv_of_isomorphism !Ex0)) fE10,
+  end
+
+  end
+
+end temp
diff --git a/cohomology/serre.hlean b/cohomology/serre.hlean
index 943c34c..e84db26 100644
--- a/cohomology/serre.hlean
+++ b/cohomology/serre.hlean
@@ -187,6 +187,12 @@ section atiyah_hirzebruch
       exact ppi_pequiv_right (λx, ptrunc_pequiv (maxm2 (s₀ + k)) (Y x k)),
     end
 
+-- set_option pp.metavar_args true
+--   definition atiyah_reindexed : (λp q, opH^p[(x : X), πₛ[q] (Y x)]) ⟹ᵍ (λn, pH^n[(x : X), Y x])
+-- :=
+--   converges_to_reindex atiyah_hirzebruch_convergence (λp q, -(p - q)) (λp q, q) (λp q, by reflexivity)
+--     (λn, -n) (λn, by reflexivity)
+
 end atiyah_hirzebruch
 
 section unreduced_atiyah_hirzebruch
diff --git a/homotopy/wedge.hlean b/homotopy/wedge.hlean
index d971bc3..2e30696 100644
--- a/homotopy/wedge.hlean
+++ b/homotopy/wedge.hlean
@@ -2,10 +2,49 @@
 
 import homotopy.wedge
 
-open wedge pushout eq prod sum pointed equiv is_equiv unit lift
+open wedge pushout eq prod sum pointed equiv is_equiv unit lift bool option
 
 namespace wedge
 
+variable (A : Type*)
+variables {A}
+
+
+definition add_point_of_wedge_pbool [unfold 2]
+  (x : A ∨ pbool) : A₊ :=
+begin
+  induction x with a b,
+  { exact some a },
+  { induction b, exact some pt, exact none },
+  { reflexivity }
+end
+
+definition wedge_pbool_of_add_point [unfold 2]
+  (x : A₊) : A ∨ pbool :=
+begin
+  induction x with a,
+  { exact inr tt },
+  { exact inl a }
+end
+
+variables (A)
+definition wedge_pbool_equiv_add_point [constructor] :
+  A ∨ pbool ≃ A₊ :=
+equiv.MK add_point_of_wedge_pbool wedge_pbool_of_add_point
+  abstract begin
+    intro x, induction x,
+    { reflexivity },
+    { reflexivity }
+  end end
+  abstract begin
+    intro x, induction x with a b,
+    { reflexivity },
+    { induction b, exact wedge.glue, reflexivity },
+    { apply eq_pathover_id_right,
+      refine ap_compose wedge_pbool_of_add_point _ _ ⬝ ap02 _ !elim_glue ⬝ph _,
+      exact square_of_eq idp }
+  end end
+
   definition wedge_flip' [unfold 3] {A B : Type*} (x : A ∨ B) : B ∨ A :=
   begin
     induction x,
@@ -14,7 +53,6 @@ namespace wedge
     { exact (glue ⋆)⁻¹ }
   end
 
-  -- TODO: fix precedences
   definition wedge_flip [constructor] (A B : Type*) : A ∨ B →* B ∨ A :=
   pmap.mk wedge_flip' (glue ⋆)⁻¹
 
diff --git a/move_to_lib.hlean b/move_to_lib.hlean
index c7ab7ff..d5a8299 100644
--- a/move_to_lib.hlean
+++ b/move_to_lib.hlean
@@ -11,6 +11,14 @@ attribute ap010 [unfold 7]
   -- TODO: homotopy_of_eq and apd10 should be the same
   -- TODO: there is also apd10_eq_of_homotopy in both pi and eq(?)
 
+namespace algebra
+
+variables {A : Type} [add_ab_inf_group A]
+definition add_sub_cancel_middle (a b : A) : a + (b - a) = b :=
+!add.comm ⬝ !sub_add_cancel
+
+end algebra
+
 namespace eq
 
   definition apd10_prepostcompose_nondep {A B C D : Type} (h : C → D) {g g' : B → C} (p : g = g')
@@ -173,7 +181,12 @@ end eq open eq
 namespace nat
 
   protected definition rec_down (P : ℕ → Type) (s : ℕ) (H0 : P s) (Hs : Πn, P (n+1) → P n) : P 0 :=
-  have Hp : Πn, P n → P (pred n),
+  begin
+    induction s with s IH,
+    { exact H0 },
+    { exact IH (Hs s H0) }
+  end
+/-  have Hp : Πn, P n → P (pred n),
   begin
     intro n p, cases n with n,
     { exact p },
@@ -185,7 +198,16 @@ namespace nat
     { exact H0 },
     { exact Hp (s - n) p }
   end,
-  transport P (nat.sub_self s) (H s)
+  transport P (nat.sub_self s) (H s)-/
+
+  /- this generalizes iterate_commute -/
+  definition iterate_hsquare {A B : Type} {f : A → A} {g : B → B}
+    (h : A → B) (p : hsquare f g h h) (n : ℕ) : hsquare (f^[n]) (g^[n]) h h :=
+  begin
+    induction n with n q,
+      exact homotopy.rfl,
+      exact q ⬝htyh p
+  end
 
 end nat
 
@@ -299,6 +321,9 @@ namespace int
   definition sub_nat_le (n : ℤ) (m : ℕ) : n - m ≤ n :=
   le.intro !sub_add_cancel
 
+  definition sub_nat_lt (n : ℤ) (m : ℕ) : n - m < n + 1 :=
+  add_le_add_right (sub_nat_le n m) 1
+
   definition sub_one_le (n : ℤ) : n - 1 ≤ n :=
   sub_nat_le n 1
 
@@ -573,6 +598,14 @@ namespace function
   variables {A B : Type} {f f' : A → B}
   open is_conn sigma.ops
 
+  definition is_contr_of_is_surjective (f : A → B) (H : is_surjective f) (HA : is_contr A)
+    (HB : is_set B) : is_contr B :=
+  is_contr.mk (f !center) begin intro b, induction H b, exact ap f !is_prop.elim ⬝ p end
+
+  definition is_contr_of_is_embedding (f : A → B) (H : is_embedding f) (HB : is_prop B)
+    (a₀ : A) : is_contr A :=
+  is_contr.mk a₀ (λa, is_injective_of_is_embedding (is_prop.elim (f a₀) (f a)))
+
   definition merely_constant {A B : Type} (f : A → B) : Type :=
   Σb, Πa, merely (f a = b)
 
@@ -780,6 +813,10 @@ end
 
 
 namespace pointed
+
+  definition pbool_pequiv_add_point_unit [constructor] : pbool ≃* unit₊ :=
+  pequiv_of_equiv (bool_equiv_option_unit) idp
+
   definition to_homotopy_pt_mk {A B : Type*} {f g : A →* B} (h : f ~ g)
     (p : h pt ⬝ respect_pt g = respect_pt f) : to_homotopy_pt (phomotopy.mk h p) = p :=
   to_right_inv !eq_con_inv_equiv_con_eq p
@@ -839,6 +876,7 @@ end sum
 namespace prod
 
   infix ` ×→ `:63 := prod_functor
+  infix ` ×≃ `:63 := prod_equiv_prod
 
 end prod
 
diff --git a/spectrum/basic.hlean b/spectrum/basic.hlean
index 851c89d..21e73ec 100644
--- a/spectrum/basic.hlean
+++ b/spectrum/basic.hlean
@@ -908,6 +908,13 @@ namespace spectrum
     { apply is_contr_loop_of_is_contr, exact IH }
   end
 
+  definition is_contr_EM_spectrum (G : AbGroup) (n : ℤ) (H : is_contr G) : is_contr (EM_spectrum G n) :=
+  begin
+    cases n with n n,
+    { apply is_contr_EM n H },
+    { apply is_contr_EM_spectrum_neg G n }
+  end
+
   /- K(πₗ(Aₖ),l) ≃* K(πₙ(A),l) for l = n + k -/
   definition EM_type_pequiv_EM (A : spectrum) {n k : ℤ} {l : ℕ} (p : n + k = l) :
     EM_type (A k) l ≃* EM (πₛ[n] A) l :=