diff --git a/hott/algebra/category/adjoint.hlean b/hott/algebra/category/adjoint.hlean
index 5e44dbe51..0862139b6 100644
--- a/hott/algebra/category/adjoint.hlean
+++ b/hott/algebra/category/adjoint.hlean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 -/
 
-import algebra.category.constructions .constructions types.function arity
+import algebra.category.constructions .constructions function arity
 
 open category functor nat_trans eq is_trunc iso equiv prod trunc function
 
diff --git a/hott/algebra/e_closure.hlean b/hott/algebra/e_closure.hlean
index 9b7137c0a..97b2365db 100644
--- a/hott/algebra/e_closure.hlean
+++ b/hott/algebra/e_closure.hlean
@@ -7,7 +7,7 @@ The "equivalence closure" of a type-valued relation.
 Given a binary type-valued relation (fibration), we add reflexivity, symmetry and transitivity terms
 -/
 
-import .relation types.eq2 arity
+import .relation eq2 arity
 
 open eq
 
diff --git a/hott/algebra/hott.hlean b/hott/algebra/hott.hlean
index 430ebcb9b..d478155b1 100644
--- a/hott/algebra/hott.hlean
+++ b/hott/algebra/hott.hlean
@@ -6,7 +6,7 @@ Author: Floris van Doorn
 Theorems about algebra specific to HoTT
 -/
 
-import .group arity types.pi types.hprop_trunc
+import .group arity types.pi hprop_trunc
 
 open equiv eq equiv.ops is_trunc
 
diff --git a/hott/book.md b/hott/book.md
index 5a0d693a8..ab946b6fa 100644
--- a/hott/book.md
+++ b/hott/book.md
@@ -29,7 +29,7 @@ The rows indicate the chapters, the columns the sections.
 
 Things not in the book:
 
-* One major difference is that in this library we heavily use pathovers, so we need less theorems about transports, but instead corresponding theorems about pathovers. These are in [init.pathover](init/pathover.hlean). For higher paths there are [squares](types/cubical/square.hlean), [squareovers](types/cubical/squareover.hlean), and the rudiments of [cubes](types/cubical/cube.hlean) and [cubeovers](types/cubical/cubeover.hlean).
+* One major difference is that in this library we heavily use pathovers, so we need less theorems about transports, but instead corresponding theorems about pathovers. These are in [init.pathover](init/pathover.hlean). For higher paths there are [squares](cubical/square.hlean), [squareovers](cubical/squareover.hlean), and the rudiments of [cubes](cubical/cube.hlean) and [cubeovers](cubical/cubeover.hlean).
 
 Chapter 1: Type theory
 ---------
@@ -60,7 +60,7 @@ Chapter 2: Homotopy type theory
 - 2.8 (The unit type): special case of [init.trunc](init/trunc.hlean)
 - 2.9 (Π-types and the function extensionality axiom): [init.funext](init/funext.hlean) and [types.pi](types/pi.hlean)
 - 2.10 (Universes and the univalence axiom): [init.ua](init/ua.hlean)
-- 2.11 (Identity type): [init.equiv](init/equiv.hlean) (ap is equivalence), [types.eq](types/eq.hlean) and [types.cubical.square](types/cubical/square.hlean) (characterization of pathovers in equality types)
+- 2.11 (Identity type): [init.equiv](init/equiv.hlean) (ap is equivalence), [types.eq](types/eq.hlean) and [cubical.square](cubical/square.hlean) (characterization of pathovers in equality types)
 - 2.12 (Coproducts): [types.sum](types/sum.hlean)
 - 2.13 (Natural numbers): [types.nat.hott](types/nat/hott.hlean)
 - 2.14 (Example: equality of structures): algebra formalized in [algebra.group](algebra/group.hlean).
@@ -71,7 +71,7 @@ Chapter 3: Sets and logic
 
 - 3.1 (Sets and n-types): [init.trunc](init/trunc.hlean)
 - 3.2 (Propositions as types?): not formalized
-- 3.3 (Mere propositions): [init.trunc](init/trunc.hlean) and [types.hprop_trunc](types/hprop_trunc.hlean) (Lemma 3.3.5).
+- 3.3 (Mere propositions): [init.trunc](init/trunc.hlean) and [hprop_trunc](hprop_trunc.hlean) (Lemma 3.3.5).
 - 3.4 (Classical vs. intuitionistic logic): decidable is defined in [init.logic](init/logic.hlean)
 - 3.5 (Subsets and propositional resizing): Lemma 3.5.1 is subtype_eq in [types.sigma](types/sigma.hlean), we don't have propositional resizing as axiom yet.
 - 3.6 (The logic of mere propositions): in the corresponding file in the [types](types/types.md) folder. (is_trunc_prod is defined in [types.sigma](types/sigma.hlean))
@@ -89,7 +89,7 @@ Chapter 4: Equivalences
 - 4.3 (Bi-invertible maps): not formalized
 - 4.4 (Contractible fibers): [types.equiv](types/equiv.hlean)
 - 4.5 (On the definition of equivalences): no formalizable content
-- 4.6 (Surjections and embeddings): [types.function](types/function.hlean)
+- 4.6 (Surjections and embeddings): [function](function.hlean)
 - 4.7 (Closure properties of equivalences): not formalized
 - 4.8 (The object classifier): not formalized
 - 4.9 (Univalence implies function extensionality): [init.funext](init/funext.hlean)
@@ -126,7 +126,7 @@ Chapter 6: Higher inductive types
 Chapter 7: Homotopy n-types
 ---------
 
-- 7.1 (Definition of n-types): [init.trunc](init/trunc.hlean), [types.trunc](types/trunc.hlean), [types.sigma](types/sigma.hlean) (Theorem 7.1.8), [types.pi](types/pi.hlean) (Theorem 7.1.9), [types.hprop_trunc](types/hprop_trunc.hlean) (Theorem 7.1.10)
+- 7.1 (Definition of n-types): [init.trunc](init/trunc.hlean), [types.trunc](types/trunc.hlean), [types.sigma](types/sigma.hlean) (Theorem 7.1.8), [types.pi](types/pi.hlean) (Theorem 7.1.9), [hprop_trunc](hprop_trunc.hlean) (Theorem 7.1.10)
 - 7.2 (Uniqueness of identity proofs and Hedberg’s theorem): [init.hedberg](init/hedberg.hlean) and [types.trunc](types/trunc.hlean)
 - 7.3 (Truncations): [init.hit](init/hit.hlean), [hit.trunc](hit/trunc.hlean) and [types.trunc](types/trunc.hlean)
 - 7.4 (Colimits of n-types): not formalized
diff --git a/hott/core.hlean b/hott/core.hlean
index 5c23ff06d..dfaa9b191 100644
--- a/hott/core.hlean
+++ b/hott/core.hlean
@@ -7,5 +7,6 @@ The core of the HoTT library
 -/
 
 import types
+import cubical
 import hit.circle
 import algebra.hott
diff --git a/hott/types/cubical/cube.hlean b/hott/cubical/cube.hlean
similarity index 100%
rename from hott/types/cubical/cube.hlean
rename to hott/cubical/cube.hlean
diff --git a/hott/types/cubical/cubeover.hlean b/hott/cubical/cubeover.hlean
similarity index 100%
rename from hott/types/cubical/cubeover.hlean
rename to hott/cubical/cubeover.hlean
diff --git a/hott/types/cubical/cubical.md b/hott/cubical/cubical.md
similarity index 63%
rename from hott/types/cubical/cubical.md
rename to hott/cubical/cubical.md
index 47bbd7d7d..4008f1ff0 100644
--- a/hott/types/cubical/cubical.md
+++ b/hott/cubical/cubical.md
@@ -3,7 +3,7 @@ types.cubical
 
 Cubical Types:
 
-The files [path](../../init/path.hlean) and [pathover](../../init/pathover.hlean) are in the [init/](../../init/init.md) folder.
+The files [path](../init/path.hlean) and [pathover](../init/pathover.hlean) are in the [init/](../init/init.md) folder.
 
 * [square](square.hlean): square in a type
 * [cube](cube.hlean): cube in a type
diff --git a/hott/types/cubical/default.hlean b/hott/cubical/default.hlean
similarity index 100%
rename from hott/types/cubical/default.hlean
rename to hott/cubical/default.hlean
diff --git a/hott/types/cubical/square.hlean b/hott/cubical/square.hlean
similarity index 100%
rename from hott/types/cubical/square.hlean
rename to hott/cubical/square.hlean
diff --git a/hott/types/cubical/squareover.hlean b/hott/cubical/squareover.hlean
similarity index 100%
rename from hott/types/cubical/squareover.hlean
rename to hott/cubical/squareover.hlean
diff --git a/hott/types/eq2.hlean b/hott/eq2.hlean
similarity index 100%
rename from hott/types/eq2.hlean
rename to hott/eq2.hlean
diff --git a/hott/types/function.hlean b/hott/function.hlean
similarity index 98%
rename from hott/types/function.hlean
rename to hott/function.hlean
index 1eb9e4855..bf0bace4e 100644
--- a/hott/types/function.hlean
+++ b/hott/function.hlean
@@ -7,7 +7,7 @@ Ported from Coq HoTT
 Theorems about embeddings and surjections
 -/
 
-import hit.trunc .pi .fiber .equiv
+import hit.trunc types.equiv
 
 open equiv sigma sigma.ops eq trunc is_trunc pi is_equiv fiber prod
 
diff --git a/hott/hit/interval.hlean b/hott/hit/interval.hlean
index 640b34d23..05bb96132 100644
--- a/hott/hit/interval.hlean
+++ b/hott/hit/interval.hlean
@@ -6,7 +6,7 @@ Authors: Floris van Doorn
 Declaration of the interval
 -/
 
-import .susp types.eq types.prod types.cubical.square
+import .susp types.eq types.prod cubical.square
 open eq susp unit equiv equiv.ops is_trunc nat prod
 
 definition interval : Type₀ := susp unit
diff --git a/hott/hit/refl_quotient.hlean b/hott/hit/refl_quotient.hlean
index 374beaf89..9ae299935 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 types.cubical.squareover .two_quotient
+import hit.circle cubical.squareover .two_quotient
 
 open eq simple_two_quotient e_closure
 
diff --git a/hott/hit/susp.hlean b/hott/hit/susp.hlean
index c06c9abcd..21d02d2fa 100644
--- a/hott/hit/susp.hlean
+++ b/hott/hit/susp.hlean
@@ -6,7 +6,7 @@ Authors: Floris van Doorn
 Declaration of suspension
 -/
 
-import .pushout types.pointed types.cubical.square
+import .pushout types.pointed cubical.square
 
 open pushout unit eq equiv equiv.ops
 
diff --git a/hott/hit/two_quotient.hlean b/hott/hit/two_quotient.hlean
index a6072a28c..f7c810600 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 types.eq2 algebra.e_closure types.cubical.cube
+import hit.circle eq2 algebra.e_closure cubical.cube
 
 open quotient eq circle sum sigma equiv function relation
 
diff --git a/hott/hott.md b/hott/hott.md
index 0c74a146e..2045f00c3 100644
--- a/hott/hott.md
+++ b/hott/hott.md
@@ -1,14 +1,19 @@
 The Lean Homotopy Type Theory Library
 =====================================
 
-The Lean homotopy type theory library is contained in the following
-files and directories:
+The Lean Homotopy Type Theory library consists of the following directories:
 
 * [init](init/init.md) : constants and theorems needed for low-level system operations
 * [types](types/types.md) : concrete datatypes and type constructors
 * [hit](hit/hit.md): higher inductive types
 * [algebra](algebra/algebra.md) : algebraic structures
-* [arity](arity.hlean) : a file containing theorems about functions with arity 2 or higher
+* [cubical](cubical/cubical.md): cubical types
+
+The following files don't fit in any of the subfolders:
+* [hprop_trunc](hprop_trunc.hlean): in this file we prove that `is_trunc n A` is a mere proposition. We separate this from [types.trunc](types/trunc.hlean) to avoid circularity in imports.
+* [eq2](eq2.hlean): coherence rules for the higher dimensional structure of equality
+* [function](function.hlean): embeddings, (split) surjections, retractions
+* [arity](arity.hlean) : equality theorems about functions with arity 2 or higher
 
 See [book.md](book.md) for an overview of the sections of the [HoTT book](http://homotopytypetheory.org/book/) which have been covered.
 
diff --git a/hott/types/hprop_trunc.hlean b/hott/hprop_trunc.hlean
similarity index 99%
rename from hott/types/hprop_trunc.hlean
rename to hott/hprop_trunc.hlean
index 4c5c4ec15..6112166c0 100644
--- a/hott/types/hprop_trunc.hlean
+++ b/hott/hprop_trunc.hlean
@@ -8,7 +8,7 @@ We prove this here to avoid circular dependency of files
 We want to use this in .equiv; .equiv is imported by .function and .function is imported by .trunc
 -/
 
-import .pi
+import types.pi
 
 open equiv sigma sigma.ops eq function pi
 
diff --git a/hott/types/default.hlean b/hott/types/default.hlean
index 1465d3c79..cc59ea54b 100644
--- a/hott/types/default.hlean
+++ b/hott/types/default.hlean
@@ -5,5 +5,5 @@ Authors: Floris van Doorn
 -/
 
 import .bool .prod .sigma .pi .arrow .pointed .fiber
-import .nat .int .cubical
-import .eq .equiv .function .trunc
+import .nat .int
+import .eq .equiv .trunc
diff --git a/hott/types/equiv.hlean b/hott/types/equiv.hlean
index fbf1e87c3..53c39e9fa 100644
--- a/hott/types/equiv.hlean
+++ b/hott/types/equiv.hlean
@@ -7,7 +7,7 @@ Ported from Coq HoTT
 Theorems about the types equiv and is_equiv
 -/
 
-import .fiber .arrow arity .hprop_trunc
+import .fiber .arrow arity ..hprop_trunc
 
 open eq is_trunc sigma sigma.ops pi fiber function equiv equiv.ops
 
diff --git a/hott/types/trunc.hlean b/hott/types/trunc.hlean
index 66a7b421a..fddcd441b 100644
--- a/hott/types/trunc.hlean
+++ b/hott/types/trunc.hlean
@@ -8,7 +8,7 @@ Properties of is_trunc and trunctype
 
 -- NOTE: the fact that (is_trunc n A) is a mere proposition is proved in .hprop_trunc
 
-import types.pi types.eq types.equiv .function
+import types.pi types.eq types.equiv ..function
 
 open eq sigma sigma.ops pi function equiv is_trunc.trunctype
      is_equiv prod is_trunc.trunc_index pointed nat
diff --git a/hott/types/types.md b/hott/types/types.md
index e5a5c8886..d53872303 100644
--- a/hott/types/types.md
+++ b/hott/types/types.md
@@ -16,14 +16,9 @@ Types (not necessarily HoTT-related):
 
 HoTT types
 
-* [hprop_trunc](hprop_trunc.hlean): in this file we prove that `is_trunc n A` is a mere proposition. We separate this from [trunc](trunc.hlean) to avoid circularity in imports.
 * [eq](eq.hlean): show that functions related to the identity type are equivalences
-* [eq2](eq2.hlean): higher dimensional structure of equality
 * [pointed](pointed.hlean)
 * [fiber](fiber.hlean)
 * [equiv](equiv.hlean)
-* [function](function.hlean): embeddings, (split) surjections, retractions
 * [trunc](trunc.hlean): truncation levels, n-Types, truncation
-* [cubical](cubical/cubical.md): cubical types (subfolder)
-