diff --git a/hott/core.hlean b/hott/core.hlean
index 42d8c5706..3bdb9fbaa 100644
--- a/hott/core.hlean
+++ b/hott/core.hlean
@@ -9,3 +9,5 @@ The core of the HoTT library
 -/
 
 import types
+import cubical.pathover cubical.square
+import hit.circle
diff --git a/hott/types/default.hlean b/hott/types/default.hlean
index 5c082671c..48739ad73 100644
--- a/hott/types/default.hlean
+++ b/hott/types/default.hlean
@@ -7,3 +7,4 @@ Authors: Floris van Doorn
 -/
 
 import .sigma .prod .pi .equiv .fiber .eq .trunc .arrow .pointed .function .trunc .bool
+import .nat .int