diff --git a/algebra/arrow_group.hlean b/algebra/arrow_group.hlean
index 15853ff..16d2aa7 100644
--- a/algebra/arrow_group.hlean
+++ b/algebra/arrow_group.hlean
@@ -7,7 +7,7 @@ Various groups of maps. Most importantly we define a group structure
 on trunc 0 (A →* Ω B), which is used in the definition of cohomology.
 -/
 
-import algebra.group_theory ..pointed ..pointed_pi eq2 homotopy.susp
+import algebra.group_theory ..pointed ..pointed_pi eq2
 open pi pointed algebra group eq equiv is_trunc trunc susp
 namespace group
 
diff --git a/homotopy/cohomology.hlean b/cohomology/basic.hlean
similarity index 99%
rename from homotopy/cohomology.hlean
rename to cohomology/basic.hlean
index b375478..07b1f55 100644
--- a/homotopy/cohomology.hlean
+++ b/cohomology/basic.hlean
@@ -6,7 +6,7 @@ Authors: Floris van Doorn, Ulrik Buchholtz
 Reduced cohomology of spectra and cohomology theories
 -/
 
-import .spectrum ..algebra.arrow_group .fwedge ..choice .pushout ..algebra.product_group
+import ..homotopy.spectrum ..algebra.arrow_group homotopy.fwedge ..choice ..homotopy.pushout ..algebra.product_group
 
 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
diff --git a/homotopy/cofiber_sequence.hlean b/cohomology/cofiber_sequence.hlean
similarity index 99%
rename from homotopy/cofiber_sequence.hlean
rename to cohomology/cofiber_sequence.hlean
index 9dfe53d..7d99f53 100644
--- a/homotopy/cofiber_sequence.hlean
+++ b/cohomology/cofiber_sequence.hlean
@@ -6,7 +6,7 @@ Authors: Floris van Doorn
 Cofiber sequence of a pointed map
 -/
 
-import .cohomology .pushout
+import .basic ..homotopy.pushout
 
 open pointed eq cohomology sigma sigma.ops fiber cofiber chain_complex nat succ_str algebra prod group pushout int
 
diff --git a/homotopy/serre.hlean b/cohomology/serre.hlean
similarity index 99%
rename from homotopy/serre.hlean
rename to cohomology/serre.hlean
index dfef176..12f2339 100644
--- a/homotopy/serre.hlean
+++ b/cohomology/serre.hlean
@@ -1,4 +1,4 @@
-import ..algebra.spectral_sequence .strunc .cohomology
+import ..algebra.spectral_sequence ..homotopy.strunc .basic
 
 open eq spectrum trunc is_trunc pointed int EM algebra left_module fiber lift equiv is_equiv
      cohomology group sigma unit is_conn
diff --git a/heq.hlean b/heq.hlean
index 8c070f8..2fabb74 100644
--- a/heq.hlean
+++ b/heq.hlean
@@ -1,3 +1,4 @@
+-- Author: Floris van Doorn
 
 open eq is_trunc
 
diff --git a/homology/homology.hlean b/homology/basic.hlean
similarity index 100%
rename from homology/homology.hlean
rename to homology/basic.hlean
diff --git a/homology/sphere.hlean b/homology/sphere.hlean
index e428191..a22abbe 100644
--- a/homology/sphere.hlean
+++ b/homology/sphere.hlean
@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Kuen-Bang Hou (Favonia)
 -/
 
-import .homology
+import .basic
 
 open eq pointed group algebra circle sphere nat equiv susp
      function sphere homology int lift
diff --git a/homology/torus.hlean b/homology/torus.hlean
index d7c7137..4525ad8 100644
--- a/homology/torus.hlean
+++ b/homology/torus.hlean
@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Kuen-Bang Hou (Favonia)
 -/
 
-import .homology .sphere ..susp_product
+import .basic .sphere ..homotopy.susp_product
 
 open eq pointed group algebra circle sphere nat equiv susp
      function sphere homology int lift prod smash
diff --git a/susp_product.hlean b/homotopy/susp_product.hlean
similarity index 79%
rename from susp_product.hlean
rename to homotopy/susp_product.hlean
index 7c31e4b..d1e901b 100644
--- a/susp_product.hlean
+++ b/homotopy/susp_product.hlean
@@ -1,4 +1,4 @@
-import core
+import homotopy.susp homotopy.smash
 open susp smash pointed wedge prod
 
 definition susp_product (X Y : Type*) : ⅀ (X × Y) ≃* ⅀ X ∨ (⅀ Y ∨ ⅀ (X ∧ Y)) :=