diff --git a/homotopy/homology.hlean b/homology/homology.hlean
similarity index 85%
rename from homotopy/homology.hlean
rename to homology/homology.hlean
index a0627ec..f5649aa 100644
--- a/homotopy/homology.hlean
+++ b/homology/homology.hlean
@@ -1,11 +1,12 @@
-import .spectrum .EM ..algebra.arrow_group ..algebra.direct_sum .fwedge ..choice .pushout ..move_to_lib ..algebra.product_group
+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
+     function fwedge cofiber bool lift sigma is_equiv choice pushout algebra unit pi smash
 
 namespace homology
 
 /- 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)
diff --git a/homotopy/spectrum.hlean b/homotopy/spectrum.hlean
index 3fa2dc4..0cf3cf0 100644
--- a/homotopy/spectrum.hlean
+++ b/homotopy/spectrum.hlean
@@ -422,8 +422,7 @@ namespace spectrum
   by induction k with k f; reflexivity; exact f ⬝e* loopn_pequiv_loopn k (equiv_glue X (n +' k))
                                                 ⬝e* !loopn_succ_in⁻¹ᵉ*
 
-  definition spectrify_map {N : succ_str} {X : gen_prespectrum N} {Y : gen_spectrum N}
-    (f : X →ₛ Y) : X →ₛ spectrify X :=
+  definition spectrify_map {N : succ_str} {X : gen_prespectrum N} : X →ₛ spectrify X :=
   begin
     fapply smap.mk,
     { intro n, exact pinclusion _ 0 },