From dcf0327e98b0b4c9b1b267c75b572d87582fccb9 Mon Sep 17 00:00:00 2001
From: favonia <favonia@gmail.com>
Date: Tue, 6 Jun 2017 11:17:11 -0600
Subject: [PATCH] Skeleton of homology groups of spheres.

---
 homology/sphere.hlean | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)
 create mode 100644 homology/sphere.hlean

diff --git a/homology/sphere.hlean b/homology/sphere.hlean
new file mode 100644
index 0000000..30ddc15
--- /dev/null
+++ b/homology/sphere.hlean
@@ -0,0 +1,21 @@
+-- Author: Kuen-Bang Hou (Favonia)
+
+import core types.lift
+import ..homotopy.homology
+
+open eq pointed group algebra circle sphere nat equiv susp
+     function sphere homology int lift
+
+namespace homology
+
+section
+  parameter (theory : homology_theory)
+
+  open homology_theory
+
+  theorem Hsphere : Π(n : ℕ), HH theory n (plift (psphere n)) ≃g HH theory 0 (plift (psphere 0)) :=
+    sorry
+
+end
+
+end homology