diff --git a/algebra/direct_sum.hlean b/algebra/direct_sum.hlean
index e5eaf82..acc32c3 100644
--- a/algebra/direct_sum.hlean
+++ b/algebra/direct_sum.hlean
@@ -12,32 +12,27 @@ open eq algebra is_trunc set_quotient relation sigma prod sum list trunc functio
 
 namespace group
 
-  variables {G G' : AddGroup} (H : subgroup_rel G) (N : normal_subgroup_rel G) {g g' h h' k : G}
-            {A B : AddAbGroup}
-
-  variables (X : Set) {l l' : list (X ⊎ X)}
-
   section
 
-    parameters {I : Set} (Y : I → AddAbGroup)
-    variables {A' : AddAbGroup} {Y' : I → AddAbGroup}
+    parameters {I : Type} [is_set I] (Y : I → AbGroup)
+    variables {A' : AbGroup} {Y' : I → AbGroup}
 
-    definition dirsum_carrier : AddAbGroup := free_ab_group (trunctype.mk (Σi, Y i) _)
+    definition dirsum_carrier : AbGroup := free_ab_group (Σi, Y i)
     local abbreviation ι [constructor] := @free_ab_group_inclusion
     inductive dirsum_rel : dirsum_carrier → Type :=
-    | rmk : Πi y₁ y₂, dirsum_rel (ι ⟨i, y₁⟩ + ι ⟨i, y₂⟩ +  -(ι ⟨i, y₁ + y₂⟩))
+    | rmk : Πi y₁ y₂, dirsum_rel (ι ⟨i, y₁⟩ * ι ⟨i, y₂⟩ *  (ι ⟨i, y₁ * y₂⟩)⁻¹)
 
-    definition dirsum : AddAbGroup := quotient_ab_group_gen dirsum_carrier (λg, ∥dirsum_rel g∥)
+    definition dirsum : AbGroup := quotient_ab_group_gen dirsum_carrier (λg, ∥dirsum_rel g∥)
 
-    -- definition dirsum_carrier_incl [constructor] (i : I) : Y i →a dirsum_carrier :=
+    -- definition dirsum_carrier_incl [constructor] (i : I) : Y i →g dirsum_carrier :=
 
-    definition dirsum_incl [constructor] (i : I) : Y i →a dirsum :=
-    add_homomorphism.mk (λy, class_of (ι ⟨i, y⟩))
+    definition dirsum_incl [constructor] (i : I) : Y i →g dirsum :=
+    homomorphism.mk (λy, class_of (ι ⟨i, y⟩))
       begin intro g h, symmetry, apply gqg_eq_of_rel, apply tr, apply dirsum_rel.rmk end
 
     parameter {Y}
     definition dirsum.rec {P : dirsum → Type} [H : Πg, is_prop (P g)]
-      (h₁ : Πi (y : Y i), P (dirsum_incl i y)) (h₂ : P 0) (h₃ : Πg h, P g → P h → P (g + h)) :
+      (h₁ : Πi (y : Y i), P (dirsum_incl i y)) (h₂ : P 1) (h₃ : Πg h, P g → P h → P (g * h)) :
       Πg, P g :=
     begin
       refine @set_quotient.rec_prop _ _ _ H _,
@@ -49,42 +44,42 @@ namespace group
         exact h₃ _ _ (h₁ i y) ih,
       induction v with i y,
       refine h₃ (gqg_map _ _ (class_of [inr ⟨i, y⟩])) _ _ ih,
-      refine transport P _ (h₁ i (-y)),
+      refine transport P _ (h₁ i y⁻¹),
       refine _ ⬝ !one_mul,
       refine _ ⬝ ap (λx, mul x _) (to_respect_zero (dirsum_incl i)),
       apply gqg_eq_of_rel',
       apply tr, esimp,
-      refine transport dirsum_rel _ (dirsum_rel.rmk i (-y) y),
-      rewrite [add.left_inv, add.assoc],
+      refine transport dirsum_rel _ (dirsum_rel.rmk i y⁻¹ y),
+      rewrite [mul.left_inv, mul.assoc],
     end
 
-    definition dirsum_homotopy {φ ψ : dirsum →a A'}
+    definition dirsum_homotopy {φ ψ : dirsum →g A'}
       (h : Πi (y : Y i), φ (dirsum_incl i y) = ψ (dirsum_incl i y)) : φ ~ ψ :=
     begin
       refine dirsum.rec _ _ _,
           exact h,
         refine !to_respect_zero ⬝ !to_respect_zero⁻¹,
-      intro g₁ g₂ h₁ h₂, rewrite [+ to_respect_add', h₁, h₂]
+      intro g₁ g₂ h₁ h₂, rewrite [* to_respect_mul, h₁, h₂]
     end
 
-    definition dirsum_elim_resp_quotient (f : Πi, Y i →a A') (g : dirsum_carrier)
+    definition dirsum_elim_resp_quotient (f : Πi, Y i →g A') (g : dirsum_carrier)
       (r : ∥dirsum_rel g∥) : free_ab_group_elim (λv, f v.1 v.2) g = 1 :=
     begin
       induction r with r, induction r,
-      rewrite [to_respect_add, to_respect_neg, to_respect_add, ▸*, ↑foldl, +one_mul,
-        to_respect_add'], apply mul.right_inv
+      rewrite [to_respect_mul, to_respect_inv, to_respect_mul, ▸*, ↑foldl, *one_mul,
+        to_respect_mul], apply mul.right_inv
     end
 
-    definition dirsum_elim [constructor] (f : Πi, Y i →a A') : dirsum →a A' :=
+    definition dirsum_elim [constructor] (f : Πi, Y i →g A') : dirsum →g A' :=
     gqg_elim _ (free_ab_group_elim (λv, f v.1 v.2)) (dirsum_elim_resp_quotient f)
 
-    definition dirsum_elim_compute (f : Πi, Y i →a A') (i : I) :
+    definition dirsum_elim_compute (f : Πi, Y i →g A') (i : I) :
       dirsum_elim f ∘g dirsum_incl i ~ f i :=
     begin
-      intro g, apply zero_add
+      intro g, apply one_mul
     end
 
-    definition dirsum_elim_unique (f : Πi, Y i →a A') (k : dirsum →a A')
+    definition dirsum_elim_unique (f : Πi, Y i →g A') (k : dirsum →g A')
       (H : Πi, k ∘g dirsum_incl i ~ f i) : k ~ dirsum_elim f :=
     begin
       apply gqg_elim_unique,
@@ -94,12 +89,12 @@ namespace group
 
   end
 
-  variables {I J : Set} {Y Y' Y'' : I → AddAbGroup}
+  variables {I J : Set} {Y Y' Y'' : I → AbGroup}
 
-  definition dirsum_functor [constructor] (f : Πi, Y i →a Y' i) : dirsum Y →a dirsum Y' :=
+  definition dirsum_functor [constructor] (f : Πi, Y i →g Y' i) : dirsum Y →g dirsum Y' :=
   dirsum_elim (λi, dirsum_incl Y' i ∘g f i)
 
-  theorem dirsum_functor_compose (f' : Πi, Y' i →a Y'' i) (f : Πi, Y i →a Y' i) :
+  theorem dirsum_functor_compose (f' : Πi, Y' i →g Y'' i) (f : Πi, Y i →g Y' i) :
     dirsum_functor f' ∘a dirsum_functor f ~ dirsum_functor (λi, f' i ∘a f i) :=
   begin
     apply dirsum_homotopy,
@@ -107,29 +102,29 @@ namespace group
   end
 
   variable (Y)
-  definition dirsum_functor_gid : dirsum_functor (λi, aid (Y i)) ~ aid (dirsum Y) :=
+  definition dirsum_functor_gid : dirsum_functor (λi, gid (Y i)) ~ gid (dirsum Y) :=
   begin
     apply dirsum_homotopy,
     intro i y, reflexivity,
   end
   variable {Y}
 
-  definition dirsum_functor_add (f f' : Πi, Y i →a Y' i) :
-    homomorphism_add (dirsum_functor f) (dirsum_functor f') ~
-    dirsum_functor (λi, homomorphism_add (f i) (f' i)) :=
+  definition dirsum_functor_mul (f f' : Πi, Y i →g Y' i) :
+    homomorphism_mul (dirsum_functor f) (dirsum_functor f') ~
+    dirsum_functor (λi, homomorphism_mul (f i) (f' i)) :=
   begin
     apply dirsum_homotopy,
     intro i y, esimp, exact sorry
   end
 
-  definition dirsum_functor_homotopy {f f' : Πi, Y i →a Y' i} (p : f ~2 f') :
+  definition dirsum_functor_homotopy {f f' : Πi, Y i →g Y' i} (p : f ~2 f') :
     dirsum_functor f ~ dirsum_functor f' :=
   begin
     apply dirsum_homotopy,
     intro i y, exact sorry
   end
 
-  definition dirsum_functor_left [constructor] (f : J → I) : dirsum (Y ∘ f) →a dirsum Y :=
+  definition dirsum_functor_left [constructor] (f : J → I) : dirsum (Y ∘ f) →g dirsum Y :=
   dirsum_elim (λj, dirsum_incl Y (f j))
 
 end group
diff --git a/algebra/free_commutative_group.hlean b/algebra/free_commutative_group.hlean
index 759be30..d34fef9 100644
--- a/algebra/free_commutative_group.hlean
+++ b/algebra/free_commutative_group.hlean
@@ -15,7 +15,7 @@ namespace group
 
   variables {G G' : Group} {g g' h h' k : G} {A B : AbGroup}
 
-  variables (X : Set) {Y : Set} {l l' : list (X ⊎ X)}
+  variables (X : Type) {Y : Type} [is_set X] [is_set Y] {l l' : list (X ⊎ X)}
 
   /- Free Abelian Group of a set -/
   namespace free_ab_group
diff --git a/algebra/free_group.hlean b/algebra/free_group.hlean
index 125332d..e8f53c0 100644
--- a/algebra/free_group.hlean
+++ b/algebra/free_group.hlean
@@ -15,7 +15,7 @@ namespace group
   variables {G G' : Group} {g g' h h' k : G} {A B : AbGroup}
 
   /- Free Group of a set -/
-  variables (X : Set) {l l' : list (X ⊎ X)}
+  variables (X : Type) [is_set X] {l l' : list (X ⊎ X)}
   namespace free_group
 
   inductive free_group_rel : list (X ⊎ X) → list (X ⊎ X) → Type :=
@@ -123,7 +123,7 @@ namespace group
   definition free_group_inclusion [constructor] (x : X) : free_group X :=
   class_of [inl x]
 
-  definition fgh_helper [unfold 5] (f : X → G) (g : G) (x : X + X) : G :=
+  definition fgh_helper [unfold 6] (f : X → G) (g : G) (x : X + X) : G :=
   g * sum.rec (λx, f x) (λx, (f x)⁻¹) x
 
   theorem fgh_helper_respect_rel (f : X → G) (r : free_group_rel X l l')
diff --git a/algebra/graded.hlean b/algebra/graded.hlean
index e7a5053..a34dd62 100644
--- a/algebra/graded.hlean
+++ b/algebra/graded.hlean
@@ -391,7 +391,7 @@ dirsum_functor (λi, smul_homomorphism (N i) r)
 definition dirsum_smul_right_distrib (r s : R) (n : dirsum' N) :
   dirsum_smul (r + s) n = dirsum_smul r n + dirsum_smul s n :=
 begin
-  refine dirsum_functor_homotopy _ n ⬝ !dirsum_functor_add⁻¹,
+  refine dirsum_functor_homotopy _ n ⬝ !dirsum_functor_mul⁻¹,
   intro i ni, exact to_smul_right_distrib r s ni
 end
 
diff --git a/algebra/seq_colim.hlean b/algebra/seq_colim.hlean
new file mode 100644
index 0000000..76b1491
--- /dev/null
+++ b/algebra/seq_colim.hlean
@@ -0,0 +1,33 @@
+import .direct_sum .quotient_group
+
+open eq algebra is_trunc set_quotient relation sigma prod sum list trunc function equiv sigma.ops nat
+
+namespace group
+
+  section
+
+    parameters (A : @trunctype.mk 0 ℕ _ → AbGroup) (f : Πi , A i → A (i + 1))
+    variables {A' : AbGroup}
+
+    definition seq_colim_carrier : AbGroup := dirsum A
+    inductive seq_colim_rel : seq_colim_carrier → Type :=
+    | rmk : Πi a, seq_colim_rel ((dirsum_incl A i a) * (dirsum_incl A (i + 1) (f i a))⁻¹)
+
+    definition seq_colim : AbGroup := quotient_ab_group_gen seq_colim_carrier (λa, ∥seq_colim_rel a∥)
+
+    definition seq_colim_incl [constructor] (i : ℕ) : A i →g seq_colim :=
+      qg_map _ ∘g dirsum_incl A i
+
+    definition seq_colim_quotient (h : Πi, A i →g A') (k : Πi a, h i a = h (i + 1) (f i a))
+                                  (v : seq_colim_carrier) (r : ∥seq_colim_rel v∥) : dirsum_elim h v = 1 :=
+      begin
+        induction r with r, induction r, exact sorry
+      end
+
+    definition seq_colim_elim [constructor] (h : Πi, A i →g A')
+                                            (k : Πi a, h i a = h (i + 1) (f i a)) : seq_colim →g A' :=
+      gqg_elim _ (dirsum_elim h) (seq_colim_quotient h k)
+
+  end
+
+end group
diff --git a/colim.hlean b/colim.hlean
index 5aaf1b5..e772352 100644
--- a/colim.hlean
+++ b/colim.hlean
@@ -1,6 +1,6 @@
 -- authors: Floris van Doorn, Egbert Rijke
 
-import hit.colimit types.fin homotopy.chain_complex .move_to_lib
+import hit.colimit types.fin homotopy.chain_complex types.pointed2
 open seq_colim pointed algebra eq is_trunc nat is_equiv equiv sigma sigma.ops chain_complex
 
 namespace seq_colim
@@ -8,12 +8,12 @@ namespace seq_colim
   definition pseq_colim [constructor] {X : ℕ → Type*} (f : Πn, X n →* X (n+1)) : Type* :=
   pointed.MK (seq_colim f) (@sι _ _ 0 pt)
 
-  definition inclusion_pt [constructor] {X : ℕ → Type*} (f : Πn, X n →* X (n+1)) (n : ℕ)
+  definition inclusion_pt {X : ℕ → Type*} (f : Πn, X n →* X (n+1)) (n : ℕ)
     : inclusion f (Point (X n)) = Point (pseq_colim f) :=
   begin
     induction n with n p,
       reflexivity,
-      exact (ap (sι f) (respect_pt _))⁻¹ᵖ ⬝ !glue ⬝ p
+      exact (ap (sι f) (respect_pt _))⁻¹ᵖ ⬝ (!glue ⬝ p)
   end
 
   definition pinclusion [constructor] {X : ℕ → Type*} (f : Πn, X n →* X (n+1)) (n : ℕ)
@@ -249,6 +249,24 @@ namespace seq_colim
     { exact ap (ι _) !respect_pt }
   end
 
+  definition pshift_equiv_pinclusion {A : ℕ → Type*} (f : Πn, A n →* A (succ n)) (n : ℕ) :
+    psquare (pinclusion f n) (pinclusion (λn, f (n+1)) n) (f n) (pshift_equiv f)  :=
+  phomotopy.mk homotopy.rfl begin 
+    refine !idp_con ⬝ _, esimp,
+    induction n with n IH,
+    { esimp[inclusion_pt], esimp[shift_diag], exact !idp_con⁻¹ },
+    { esimp[inclusion_pt], refine !con_inv_cancel_left ⬝ _,
+      rewrite ap_con, rewrite ap_con,
+      refine _ ⬝ whisker_right _ !con.assoc,
+      refine _ ⬝ (con.assoc (_ ⬝ _) _ _)⁻¹,
+      xrewrite [-IH], 
+      esimp[shift_up], rewrite [elim_glue,  ap_inv, -ap_compose'], esimp,
+      rewrite [-+con.assoc], apply whisker_right,
+      rewrite con.assoc, apply !eq_inv_con_of_con_eq,
+      symmetry, exact eq_of_square !natural_square
+  }
+  end
+
   section functor
   variable {f}
   variables {A' : ℕ → Type} {f' : seq_diagram A'}
@@ -305,6 +323,30 @@ namespace seq_colim
     : Π(x : seq_colim f), P x :=
   by induction v with Pincl Pglue; exact seq_colim.rec f Pincl Pglue
 
+  definition pseq_colim_pequiv [constructor] {A A' : ℕ → Type*} {f : Π{n}, A n →* A (n+1)}
+    {f' : Π{n}, A' n →* A' (n+1)} (g : Π{n}, A n ≃* A' n)
+    (p : Π⦃n⦄, g ∘* f ~ f' ∘* g) : pseq_colim @f ≃* pseq_colim @f' :=
+  pequiv_of_equiv (seq_colim_equiv @g p) (ap (ι _) (respect_pt g))
+
+  definition seq_colim_equiv_constant [constructor] {A : ℕ → Type*} {f f' : Π⦃n⦄, A n → A (n+1)}
+    (p : Π⦃n⦄ (a : A n), f a = f' a) : seq_colim f ≃ seq_colim f' :=
+  seq_colim_equiv (λn, erfl) p
+
+  definition pseq_colim_equiv_constant [constructor] {A : ℕ → Type*} {f f' : Π{n}, A n →* A (n+1)}
+    (p : Π⦃n⦄, f ~ f') : pseq_colim @f ≃* pseq_colim @f' :=
+  pseq_colim_pequiv (λn, pequiv.rfl) p
+
+  definition pseq_colim_pequiv_pinclusion {A A' : ℕ → Type*} {f : Π(n), A n →* A (n+1)}
+    {f' : Π(n), A' n →* A' (n+1)} (g : Π(n), A n ≃* A' n)
+    (p : Π⦃n⦄, g (n+1) ∘* f n ~ f' n ∘* g n) (n : ℕ) :
+    psquare (pinclusion f n) (pinclusion f' n) (g n) (pseq_colim_pequiv g p) :=
+  sorry
+
+  definition seq_colim_equiv_constant_pinclusion {A : ℕ → Type*} {f f' : Π⦃n⦄, A n →* A (n+1)}
+    (p : Π⦃n⦄ (a : A n), f a = f' a) (n : ℕ) :
+    pseq_colim_equiv_constant p ∘* pinclusion f n ~* pinclusion f' n  :=
+  sorry
+
   definition is_equiv_seq_colim_rec (P : seq_colim f → Type) :
     is_equiv (seq_colim_rec_unc :
       (Σ(Pincl : Π ⦃n : ℕ⦄ (a : A n), P (ι f a)),
@@ -327,19 +369,6 @@ namespace seq_colim
   equiv.mk _ !is_equiv_seq_colim_rec
   end functor
 
-  definition pseq_colim_pequiv [constructor] {A A' : ℕ → Type*} {f : Π{n}, A n →* A (n+1)}
-    {f' : Π{n}, A' n →* A' (n+1)} (g : Π{n}, A n ≃* A' n)
-    (p : Π⦃n⦄, g ∘* f ~ f' ∘* g) : pseq_colim @f ≃* pseq_colim @f' :=
-  pequiv_of_equiv (seq_colim_equiv @g p) (ap (ι _) (respect_pt g))
-
-  definition seq_colim_equiv_constant [constructor] {A : ℕ → Type*} {f f' : Π⦃n⦄, A n → A (n+1)}
-    (p : Π⦃n⦄ (a : A n), f a = f' a) : seq_colim f ≃ seq_colim f' :=
-  seq_colim_equiv (λn, erfl) p
-
-  definition pseq_colim_equiv_constant [constructor] {A : ℕ → Type*} {f f' : Π{n}, A n →* A (n+1)}
-    (p : Π⦃n⦄, f ~ f') : pseq_colim @f ≃* pseq_colim @f' :=
-  pseq_colim_pequiv (λn, pequiv.rfl) p
-
   definition pseq_colim.elim [constructor] {A : ℕ → Type*} {B : Type*} {f : Π{n}, A n →* A (n+1)}
     (g : Πn, A n →* B) (p : Πn, g (n+1) ∘* f ~ g n) : pseq_colim @f →* B :=
   begin
@@ -361,6 +390,7 @@ namespace seq_colim
   theorem prep0_succ_lemma {A : ℕ → Type*} (f : pseq_diagram A) (n : ℕ)
     (p : rep0 (λn x, f x) n pt = rep0 (λn x, f x) n pt)
     (q : prep0 f n (Point (A 0)) = Point (A n))
+
     : loop_equiv_eq_closed (ap (@f n) q ⬝ respect_pt (@f n))
     (ap (@f n) p) = Ω→(@f n) (loop_equiv_eq_closed q p) :=
   by rewrite [▸*, con_inv, ↑ap1_gen, +ap_con, ap_inv, +con.assoc]
@@ -466,6 +496,10 @@ namespace seq_colim
     { exact sorry }
   end
 
+  definition pseq_colim_loop_pinclusion {X : ℕ → Type*} (f : Πn, X n →* X (n+1)) (n : ℕ) :
+    pseq_colim_loop f ∘* Ω→ (pinclusion f n) ~* pinclusion (λn, Ω→(f n)) n :=
+  sorry
+
   -- open succ_str
   -- definition pseq_colim_succ_str_change_index' {N : succ_str} {B : N → Type*} (n : N) (m : ℕ)
   --   (h : Πn, B n →* B (S n)) :
diff --git a/homology/homology.hlean b/homology/homology.hlean
index f5649aa..32e79f8 100644
--- a/homology/homology.hlean
+++ b/homology/homology.hlean
@@ -1,23 +1,73 @@
 import ..homotopy.spectrum ..homotopy.EM ..algebra.arrow_group ..algebra.direct_sum ..homotopy.fwedge ..choice ..homotopy.pushout ..move_to_lib
 
-open eq spectrum int trunc pointed EM group algebra circle sphere nat EM.ops equiv susp is_trunc
-     function fwedge cofiber bool lift sigma is_equiv choice pushout algebra unit pi smash
+open eq spectrum int pointed group algebra sphere nat equiv susp is_trunc
+     function fwedge cofiber lift is_equiv choice algebra pi smash
 
 namespace homology
 
-/- homology theory -/
+  /- homology theory -/
+
+  structure homology_theory.{u} : Type.{u+1} :=
+    (HH : ℤ → pType.{u} → AbGroup.{u})
+    (Hh : Π(n : ℤ) {X Y : Type*} (f : X →* Y), HH n X →g HH n Y)
+    (Hid : Π(n : ℤ) {X : Type*} (x : HH n X), Hh n (pid X) x = x)
+    (Hcompose : Π(n : ℤ) {X Y Z : Type*} (f : Y →* Z) (g : X →* Y),
+      Hh n (f ∘* g) ~ Hh n f ∘ Hh n g)
+    (Hsusp : Π(n : ℤ) (X : Type*), HH (succ n) (psusp X) ≃g HH n X)
+    (Hsusp_natural : Π(n : ℤ) {X Y : Type*} (f : X →* Y),
+      Hsusp n Y ∘ Hh (succ n) (psusp_functor f) ~ Hh n f ∘ Hsusp n X)
+    (Hexact : Π(n : ℤ) {X Y : Type*} (f : X →* Y), is_exact_g (Hh n f) (Hh n (pcod f)))
+    (Hadditive : Π(n : ℤ) {I : Set.{u}} (X : I → Type*), is_equiv
+      (dirsum_elim (λi, Hh n (pinl i)) : dirsum (λi, HH n (X i)) → HH n (⋁ X)))
+
+  section
+    parameter (theory : homology_theory)
+    open homology_theory
+
+    theorem HH_base_indep (n : ℤ) {A : Type} (a b : A)
+      : HH theory n (pType.mk A a) ≃g HH theory n (pType.mk A b) :=
+      calc HH theory n (pType.mk A a) ≃g HH theory (int.succ n) (psusp A) : by exact (Hsusp theory n (pType.mk A a)) ⁻¹ᵍ
+                                  ... ≃g HH theory n (pType.mk A b)       : by exact Hsusp theory n (pType.mk A b)
+
+    theorem Hh_homotopy' (n : ℤ) {A B : Type*} (f : A → B) (p q : f pt = pt)
+      : Hh theory n (pmap.mk f p) ~ Hh theory n (pmap.mk f q) := λ x,
+    calc       Hh theory n (pmap.mk f p) x
+             = Hh theory n (pmap.mk f p) (Hsusp theory n A ((Hsusp theory n A)⁻¹ᵍ x))
+               : by exact ap (Hh theory n (pmap.mk f p)) (equiv.to_right_inv (equiv_of_isomorphism (Hsusp theory n A)) x)⁻¹
+         ... = Hsusp theory n B (Hh theory (succ n) (pmap.mk (susp.functor f) !refl) ((Hsusp theory n A)⁻¹ x))
+               : by exact (Hsusp_natural theory n (pmap.mk f p) ((Hsusp theory n A)⁻¹ᵍ x))⁻¹
+         ... = Hh theory n (pmap.mk f q) (Hsusp theory n A ((Hsusp theory n A)⁻¹ x))
+               : by exact Hsusp_natural theory n (pmap.mk f q) ((Hsusp theory n A)⁻¹ x)
+         ... = Hh theory n (pmap.mk f q) x
+               : by exact ap (Hh theory n (pmap.mk f q)) (equiv.to_right_inv (equiv_of_isomorphism (Hsusp theory n A)) x)
+
+    theorem Hh_homotopy (n : ℤ) {A B : Type*} (f g : A →* B) (h : f ~ g) : Hh theory n f ~ Hh theory n g := λ x,
+    calc       Hh theory n f x
+             = Hh theory n (pmap.mk f (respect_pt f)) x : by exact ap (λ f, Hh theory n f x) (pmap.eta f)⁻¹
+         ... = Hh theory n (pmap.mk f (h pt ⬝ respect_pt g)) x : by exact Hh_homotopy' n f (respect_pt f) (h pt ⬝ respect_pt g) x
+         ... = Hh theory n g x : by exact ap (λ f, Hh theory n f x) (@pmap_eq _ _ (pmap.mk f (h pt ⬝ respect_pt g)) _ h (refl (h pt ⬝ respect_pt g)))
+
+    definition HH_isomorphism (n : ℤ) {A B : Type*} (e : A ≃* B)
+      : HH theory n A ≃g HH theory n B :=
+    begin
+      fapply isomorphism.mk,
+      { exact Hh theory n e },
+      fapply adjointify,
+      { exact Hh theory n e⁻¹ᵉ* },
+      { intro x, exact calc
+              Hh theory n e (Hh theory n e⁻¹ᵉ* x)
+            = Hh theory n (e ∘* e⁻¹ᵉ*) x : by exact (Hcompose theory n e e⁻¹ᵉ* x)⁻¹
+        ... = Hh theory n !pid x : by exact Hh_homotopy n (e ∘* e⁻¹ᵉ*) !pid (to_right_inv e) x
+        ... = x : by exact Hid theory n x
+      },
+      { intro x, exact calc
+              Hh theory n e⁻¹ᵉ* (Hh theory n e x)
+            = Hh theory n (e⁻¹ᵉ* ∘* e) x : by exact (Hcompose theory n e⁻¹ᵉ* e x)⁻¹
+        ... = Hh theory n !pid x : by exact Hh_homotopy n (e⁻¹ᵉ* ∘* e) !pid (to_left_inv e) x
+        ... = x : by exact Hid theory n x
+      }
+    end
+
+  end
 
-structure homology_theory.{u} : Type.{u+1} :=
-  (HH : ℤ → pType.{u} → AbGroup.{u})
-  (Hh : Π(n : ℤ) {X Y : Type*} (f : X →* Y), HH n X →g HH n Y)
-  (Hid : Π(n : ℤ) {X : Type*} (x : HH n X), Hh n (pid X) x = x)
-  (Hcompose : Π(n : ℤ) {X Y Z : Type*} (g : Y →* Z) (f : X →* Y) (x : HH n X),
-    Hh n (g ∘* f) x = Hh n g (Hh n f x))
-  (Hsusp : Π(n : ℤ) (X : Type*), HH (succ n) (psusp X) ≃g HH n X)
-  (Hsusp_natural : Π(n : ℤ) {X Y : Type*} (f : X →* Y),
-    Hsusp n Y ∘ Hh (succ n) (psusp_functor f) ~ Hh n f ∘ Hsusp n X)
-  (Hexact : Π(n : ℤ) {X Y : Type*} (f : X →* Y), is_exact_g (Hh n f) (Hh n (pcod f)))
-  (Hadditive : Π(n : ℤ) {I : Set.{u}} (X : I → Type*), is_equiv (
-    dirsum_elim (λi, Hh n (pinl i)) : dirsum (λi, HH n (X i)) → HH n (⋁ X))
-)
 end homology
diff --git a/homology/sphere.hlean b/homology/sphere.hlean
index 30ddc15..e5eb677 100644
--- a/homology/sphere.hlean
+++ b/homology/sphere.hlean
@@ -1,7 +1,7 @@
 -- Author: Kuen-Bang Hou (Favonia)
 
-import core types.lift
-import ..homotopy.homology
+import core
+import .homology
 
 open eq pointed group algebra circle sphere nat equiv susp
      function sphere homology int lift
@@ -13,9 +13,21 @@ section
 
   open homology_theory
 
-  theorem Hsphere : Π(n : ℕ), HH theory n (plift (psphere n)) ≃g HH theory 0 (plift (psphere 0)) :=
-    sorry
-
+  theorem Hsphere : Π(n : ℤ)(m : ℕ), HH theory n (plift (psphere m)) ≃g HH theory (n - m) (plift (psphere 0)) :=
+    begin
+      intros n m, revert n, induction m with m,
+      { exact λ n, isomorphism_ap (λ n, HH theory n (plift (psphere 0))) (sub_zero n)⁻¹ },
+      { intro n, exact calc
+                  HH theory n (plift (psusp (psphere m)))
+               ≃g HH theory n (psusp (plift (psphere m))) : by exact HH_isomorphism theory n (plift_psusp (psphere m))
+           ... ≃g HH theory (succ (pred n)) (psusp (plift (psphere m)))
+                  : by exact isomorphism_ap (λ n, HH theory n (psusp (plift (psphere m)))) (succ_pred n)⁻¹
+           ... ≃g HH theory (pred n) (plift (psphere m)) : by exact Hsusp theory (pred n) (plift (psphere m))
+           ... ≃g HH theory (pred n - m) (plift (psphere 0)) : by exact v_0 (pred n)
+           ... ≃g HH theory (n - succ m) (plift (psphere 0))
+                  : by exact isomorphism_ap (λ n, HH theory n (plift (psphere 0))) (sub_sub n 1 m ⬝ ap (λ m, n - m) (add.comm 1 m))
+      }
+    end
 end
 
 end homology
diff --git a/homotopy/smash.hlean b/homotopy/smash.hlean
index 4b6d875..82d5a98 100644
--- a/homotopy/smash.hlean
+++ b/homotopy/smash.hlean
@@ -5,7 +5,7 @@ import homotopy.smash types.pointed2 .pushout homotopy.red_susp
 open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber prod.ops wedge is_trunc
      function red_susp unit
 
-  /- To prove: Σ(X × Y) ≃ ΣX ∨ ΣY ∨ Σ(X ∧ Y) (?) (notation means suspension, wedge, smash) -/
+  /- To prove: Σ(X × Y) ≃ ΣX ∨ ΣY ∨ Σ(X ∧ Y) (notation means suspension, wedge, smash) -/
 
   /- To prove: Σ(X ∧ Y) ≃ X ★ Y (?) (notation means suspension, smash, join) -/
 
diff --git a/homotopy/spectrum.hlean b/homotopy/spectrum.hlean
index 735fcbc..be199dd 100644
--- a/homotopy/spectrum.hlean
+++ b/homotopy/spectrum.hlean
@@ -396,17 +396,17 @@ namespace spectrum
   definition spectrify_pequiv {N : succ_str} (X : gen_prespectrum N) (n : N) :
     spectrify_type X n ≃* Ω (spectrify_type X (S n)) :=
   begin
-    refine _ ⬝e* !pseq_colim_loop⁻¹ᵉ*,
     refine !pshift_equiv ⬝e* _,
-    transitivity pseq_colim (λk, spectrify_type_fun' X (succ k) (S n +' k)), rotate 1,
-    refine pseq_colim_equiv_constant (λn, !ap1_pcompose⁻¹*),
+    transitivity pseq_colim (λk, spectrify_type_fun' X (succ k) (S n +' k)),
     fapply pseq_colim_pequiv,
     { intro n, apply loopn_pequiv_loopn, apply pequiv_ap X, apply succ_str.add_succ },
     { intro k, apply to_homotopy,
       refine !passoc⁻¹* ⬝* _, refine pwhisker_right _ (loopn_succ_in_inv_natural (succ k) _) ⬝* _,
       refine !passoc ⬝* _ ⬝* !passoc⁻¹*, apply pwhisker_left,
       refine !apn_pcompose⁻¹* ⬝* _ ⬝* !apn_pcompose, apply apn_phomotopy,
-      exact !glue_ptransport⁻¹* }
+      exact !glue_ptransport⁻¹* },
+    refine _ ⬝e* !pseq_colim_loop⁻¹ᵉ*,
+    refine pseq_colim_equiv_constant (λn, !ap1_pcompose⁻¹*),
   end
 
   definition spectrify [constructor] {N : succ_str} (X : gen_prespectrum N) : gen_spectrum N :=
@@ -426,7 +426,14 @@ namespace spectrum
   begin
     fapply smap.mk,
     { intro n, exact pinclusion _ 0 },
-    { intro n, exact sorry }
+    { intro n, apply phomotopy_of_psquare, refine !pid_pcompose⁻¹* ⬝ph* _,
+      refine !pid_pcompose⁻¹* ⬝ph* _,
+      --pshift_equiv_pinclusion (spectrify_type_fun X n) 0
+      refine _ ⬝v* _,
+      rotate 1, exact pshift_equiv_pinclusion (spectrify_type_fun X n) 0,
+--      refine !passoc⁻¹* ⬝* pwhisker_left _ _ ⬝* _,
+      exact sorry
+}
   end
 
   definition spectrify.elim {N : succ_str} {X : gen_prespectrum N} {Y : gen_spectrum N}
diff --git a/move_to_lib.hlean b/move_to_lib.hlean
index 2f745a8..556ec6c 100644
--- a/move_to_lib.hlean
+++ b/move_to_lib.hlean
@@ -95,6 +95,13 @@ namespace eq
 
 end eq open eq
 
+namespace pmap
+
+  definition eta {A B : Type*} (f : A →* B) : pmap.mk f (respect_pt f) = f :=
+  begin induction f, reflexivity end
+
+end pmap
+
 namespace trunc
 
   -- TODO: redefine loopn_ptrunc_pequiv
@@ -170,6 +177,9 @@ namespace group
   --   : @is_mul_hom G G' (@ab_group.to_group _ (AbGroup.struct G)) _ φ :=
   -- homomorphism.struct φ
 
+  definition isomorphism_ap {A : Type} (F : A → Group) {a b : A} (p : a = b) : F a ≃g F b :=
+    isomorphism_of_eq (ap F p)
+
 end group open group
 
 namespace function
diff --git a/susp_product.hlean b/susp_product.hlean
new file mode 100644
index 0000000..3de39d6
--- /dev/null
+++ b/susp_product.hlean
@@ -0,0 +1,5 @@
+import core
+open susp smash pointed wedge prod
+
+definition susp_product (X Y : Type*) : ⅀ (X × Y) ≃* ⅀ X ∨ (⅀ Y ∨ (X ∧ Y)) :=
+  sorry