diff --git a/homology/homology.hlean b/homology/homology.hlean
index ebfa457..2f4145c 100644
--- a/homology/homology.hlean
+++ b/homology/homology.hlean
@@ -6,10 +6,10 @@ Authors: Yuri Sulyma, Favonia
 Reduced homology theories
 -/
 
-import ..homotopy.spectrum ..homotopy.EM ..algebra.arrow_group ..algebra.direct_sum ..homotopy.fwedge ..choice ..homotopy.pushout ..move_to_lib
+import ..homotopy.spectrum ..homotopy.EM ..algebra.arrow_group ..algebra.direct_sum ..homotopy.fwedge ..homotopy.wedge ..choice ..homotopy.pushout ..move_to_lib
 
 open eq spectrum int pointed group algebra sphere nat equiv susp is_trunc
-     function fwedge cofiber lift is_equiv choice algebra pi smash
+     function fwedge cofiber lift is_equiv choice algebra pi smash wedge
 
 namespace homology
 
@@ -129,6 +129,20 @@ namespace homology
                          ... ≃g HH theory n A ×g HH theory n B : by exact binary_dirsum (HH theory n A) (HH theory n B)
 
   end
+  section
+    universe variables u v
+    parameter (theory : homology_theory.{max u v})
+    open homology_theory
+
+    definition Hplift_psusp (n : ℤ) (A : Type*): HH theory (n + 1) (plift.{u v} (psusp A)) ≃g HH theory n (plift.{u v} A) :=
+    calc HH theory (n + 1) (plift.{u v} (psusp A)) ≃g HH theory (n + 1) (psusp (plift.{u v} A)) : by exact HH_isomorphism theory (n + 1) (plift_psusp _)
+                                               ... ≃g HH theory n (plift.{u v} A) : by exact Hpsusp theory n (plift.{u v} A)
+
+    definition Hplift_pwedge (n : ℤ) (A B : Type*): HH theory n (plift.{u v} (A ∨ B)) ≃g HH theory n (plift.{u v} A) ×g HH theory n (plift.{u v} B) :=
+    calc HH theory n (plift.{u v} (A ∨ B)) ≃g HH theory n (plift.{u v} A ∨ plift.{u v} B) : by exact HH_isomorphism theory n (plift_pwedge A B)
+                                       ... ≃g HH theory n (plift.{u v} A) ×g HH theory n (plift.{u v} B) : by exact Hpwedge theory n (plift.{u v} A) (plift.{u v} B)
+
+  end
 
 /- homology theory associated to a prespectrum -/
 definition homology (X : Type*) (E : prespectrum) (n : ℤ) : AbGroup :=
diff --git a/homology/sphere.hlean b/homology/sphere.hlean
index d6f789f..e428191 100644
--- a/homology/sphere.hlean
+++ b/homology/sphere.hlean
@@ -23,10 +23,9 @@ section
       { 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 Hpsusp theory (pred n) (plift (psphere m))
+               ≃g HH theory (succ (pred n)) (plift (psusp (psphere m)))
+                  : by exact isomorphism_ap (λ n, HH theory n (plift (psusp (psphere m)))) (succ_pred n)⁻¹
+           ... ≃g HH theory (pred n) (plift (psphere m)) : by exact Hplift_psusp theory (pred n) (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))
diff --git a/homology/torus.hlean b/homology/torus.hlean
new file mode 100644
index 0000000..e2bf276
--- /dev/null
+++ b/homology/torus.hlean
@@ -0,0 +1,40 @@
+/-
+Copyright (c) 2017 Kuen-Bang Hou (Favonia).
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Kuen-Bang Hou (Favonia)
+-/
+
+import .homology .sphere ..susp_product
+
+open eq pointed group algebra circle sphere nat equiv susp
+     function sphere homology int lift prod smash
+
+namespace homology
+
+section
+  parameter (theory : ordinary_homology_theory)
+
+  open ordinary_homology_theory
+
+  theorem Hptorus : Π(n : ℤ)(m : ℕ), HH theory n (plift (psphere m ×* psphere m)) ≃g
+    HH theory n (plift (psphere m)) ×g (HH theory n (plift (psphere m)) ×g HH theory n (plift (psphere (m + m)))) := λ n m,
+    calc        HH theory n (plift (psphere m ×* psphere m))
+             ≃g HH theory (n + 1) (plift (⅀ (psphere m ×* psphere m))) : by exact (Hplift_psusp theory n (psphere m ×* psphere m))⁻¹ᵍ
+         ... ≃g HH theory (n + 1) (plift (⅀ (psphere m) ∨ (⅀ (psphere m) ∨ ⅀ (psphere m ∧ psphere m))))
+                   : by exact HH_isomorphism theory (n + 1) (!pequiv_plift⁻¹ᵉ* ⬝e* susp_product (psphere m) (psphere m) ⬝e* !pequiv_plift)
+         ... ≃g HH theory (n + 1) (plift (⅀ (psphere m))) ×g HH theory (n + 1) (plift (⅀ (psphere m) ∨ (⅀ (psphere m ∧ psphere m))))
+                   : by exact Hplift_pwedge theory (n + 1) (⅀ (psphere m)) (⅀ (psphere m) ∨ (⅀ (psphere m ∧ psphere m)))
+         ... ≃g HH theory n (plift (psphere m)) ×g (HH theory n (plift (psphere m)) ×g HH theory n (plift (psphere (m + m))))
+                   : by exact product_isomorphism (Hplift_psusp theory n (psphere m))
+             (calc
+                     HH theory (n + 1) (plift (⅀ (psphere m) ∨ (⅀ (psphere m ∧ psphere m))))
+                  ≃g HH theory (n + 1) (plift (⅀ (psphere m))) ×g HH theory (n + 1) (plift (⅀ (psphere m ∧ psphere m)))
+                     : by exact Hplift_pwedge theory (n + 1) (⅀ (psphere m)) (⅀ (psphere m ∧ psphere m))
+              ... ≃g HH theory n (plift (psphere m)) ×g HH theory n (plift (psphere (m + m)))
+                     : by exact product_isomorphism (Hplift_psusp theory n (psphere m))
+                                  (Hplift_psusp theory n (psphere m ∧ psphere m) ⬝g HH_isomorphism theory n (!pequiv_plift⁻¹ᵉ* ⬝e* (sphere_smash_sphere m m) ⬝e* !pequiv_plift)))
+
+end
+
+end homology