diff --git a/src/Cat.agda b/src/Cat.agda
index edf98de..c452d26 100644
--- a/src/Cat.agda
+++ b/src/Cat.agda
@@ -1,12 +1,12 @@
 module Cat where
 
 import Cat.Category
-import Cat.Functor
 import Cat.CwF
-import Cat.CartesianClosed
-import Cat.Exponential
-import Cat.Product
 
+import Cat.Category.Functor
+import Cat.Category.Product
+import Cat.Category.Exponential
+import Cat.Category.CartesianClosed
 import Cat.Category.Pathy
 import Cat.Category.Bij
 import Cat.Category.Free
diff --git a/src/Cat/Categories/Cube.agda b/src/Cat/Categories/Cube.agda
index ee0eccc..fdee75e 100644
--- a/src/Cat/Categories/Cube.agda
+++ b/src/Cat/Categories/Cube.agda
@@ -13,7 +13,7 @@ open import Relation.Nullary
 open import Relation.Nullary.Decidable
 
 open import Cat.Category
-open import Cat.Functor
+open import Cat.Category.Functor
 open import Cat.Equality
 open Equality.Data.Product
 
diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda
index c14823a..50acaaa 100644
--- a/src/Cat/Categories/Fun.agda
+++ b/src/Cat/Categories/Fun.agda
@@ -7,7 +7,7 @@ open import Function
 open import Data.Product
 
 open import Cat.Category
-open import Cat.Functor
+open import Cat.Category.Functor
 
 module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Category ℓd ℓd'} where
   open Category hiding ( _∘_ ; Arrow )
diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda
index e9a8b87..e13fa0c 100644
--- a/src/Cat/Categories/Sets.agda
+++ b/src/Cat/Categories/Sets.agda
@@ -7,8 +7,8 @@ open import Data.Product
 import Function
 
 open import Cat.Category
-open import Cat.Functor
-open import Cat.Product
+open import Cat.Category.Functor
+open import Cat.Category.Product
 open Category
 
 module _ {ℓ : Level} where
diff --git a/src/Cat/CartesianClosed.agda b/src/Cat/Category/CartesianClosed.agda
similarity index 68%
rename from src/Cat/CartesianClosed.agda
rename to src/Cat/Category/CartesianClosed.agda
index e00fd0d..ba477c9 100644
--- a/src/Cat/CartesianClosed.agda
+++ b/src/Cat/Category/CartesianClosed.agda
@@ -1,10 +1,10 @@
-module Cat.CartesianClosed where
+module Cat.Category.CartesianClosed where
 
 open import Agda.Primitive
 
 open import Cat.Category
-open import Cat.Product
-open import Cat.Exponential
+open import Cat.Category.Product
+open import Cat.Category.Exponential
 
 record CartesianClosed {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') : Set (ℓ ⊔ ℓ') where
   field
diff --git a/src/Cat/Exponential.agda b/src/Cat/Category/Exponential.agda
similarity index 95%
rename from src/Cat/Exponential.agda
rename to src/Cat/Category/Exponential.agda
index df70399..5865da0 100644
--- a/src/Cat/Exponential.agda
+++ b/src/Cat/Category/Exponential.agda
@@ -1,11 +1,11 @@
-module Cat.Exponential where
+module Cat.Category.Exponential where
 
 open import Agda.Primitive
 open import Data.Product
 open import Cubical
 
 open import Cat.Category
-open import Cat.Product
+open import Cat.Category.Product
 
 open Category
 
diff --git a/src/Cat/Functor.agda b/src/Cat/Category/Functor.agda
similarity index 99%
rename from src/Cat/Functor.agda
rename to src/Cat/Category/Functor.agda
index 890801b..912557e 100644
--- a/src/Cat/Functor.agda
+++ b/src/Cat/Category/Functor.agda
@@ -1,4 +1,4 @@
-module Cat.Functor where
+module Cat.Category.Functor where
 
 open import Agda.Primitive
 open import Cubical
diff --git a/src/Cat/Product.agda b/src/Cat/Category/Product.agda
similarity index 98%
rename from src/Cat/Product.agda
rename to src/Cat/Category/Product.agda
index f50c36d..cbc42b5 100644
--- a/src/Cat/Product.agda
+++ b/src/Cat/Category/Product.agda
@@ -1,4 +1,4 @@
-module Cat.Product where
+module Cat.Category.Product where
 
 open import Agda.Primitive
 open import Data.Product
diff --git a/src/Cat/Category/Properties.agda b/src/Cat/Category/Properties.agda
index 2477447..9b678a5 100644
--- a/src/Cat/Category/Properties.agda
+++ b/src/Cat/Category/Properties.agda
@@ -7,7 +7,7 @@ open import Data.Product
 open import Cubical
 
 open import Cat.Category
-open import Cat.Functor
+open import Cat.Category.Functor
 open import Cat.Categories.Sets
 open import Cat.Equality
 open Equality.Data.Product
@@ -51,7 +51,6 @@ epi-mono-is-not-iso f =
 
 open import Cat.Category
 open Category
-open import Cat.Functor
 open Functor
 
 -- module _ {ℓ : Level} {ℂ : Category ℓ ℓ}
diff --git a/src/Cat/CwF.agda b/src/Cat/CwF.agda
index c3099ca..44e725e 100644
--- a/src/Cat/CwF.agda
+++ b/src/Cat/CwF.agda
@@ -4,7 +4,7 @@ open import Agda.Primitive
 open import Data.Product
 
 open import Cat.Category
-open import Cat.Functor
+open import Cat.Category.Functor
 open import Cat.Categories.Fam
 
 open Category