diff --git a/hott/core.hlean b/hott/core.hlean
index dfaa9b1918..0c35225dfa 100644
--- a/hott/core.hlean
+++ b/hott/core.hlean
@@ -8,5 +8,5 @@ The core of the HoTT library
 
 import types
 import cubical
-import hit.circle
+import homotopy.circle
 import algebra.hott
diff --git a/hott/hit/refl_quotient.hlean b/hott/hit/refl_quotient.hlean
index 9ae2999358..bc4e467843 100644
--- a/hott/hit/refl_quotient.hlean
+++ b/hott/hit/refl_quotient.hlean
@@ -7,7 +7,7 @@ Authors: Floris van Doorn
 Quotient of a reflexive relation
 -/
 
-import hit.circle cubical.squareover .two_quotient
+import homotopy.circle cubical.squareover .two_quotient
 
 open eq simple_two_quotient e_closure
 
diff --git a/hott/hit/two_quotient.hlean b/hott/hit/two_quotient.hlean
index 724cb46701..7463a5f706 100644
--- a/hott/hit/two_quotient.hlean
+++ b/hott/hit/two_quotient.hlean
@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 -/
 
-import hit.circle eq2 algebra.e_closure cubical.cube
+import homotopy.circle eq2 algebra.e_closure cubical.cube
 
 open quotient eq circle sum sigma equiv function relation
 
diff --git a/hott/homotopy/cellcomplex.hlean b/hott/homotopy/cellcomplex.hlean
index e69a21982b..63a45400f9 100644
--- a/hott/homotopy/cellcomplex.hlean
+++ b/hott/homotopy/cellcomplex.hlean
@@ -3,7 +3,7 @@ Copyright (c) 2015 Ulrik Buchholtz. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Ulrik Buchholtz
 -/
-import types.trunc hit.sphere hit.pushout
+import types.trunc homotopy.sphere hit.pushout
 
 open eq is_trunc is_equiv nat equiv trunc prod pushout sigma sphere_index unit