diff --git a/src/Cat.agda b/src/Cat.agda
index 1319eb6..cf6a174 100644
--- a/src/Cat.agda
+++ b/src/Cat.agda
@@ -1,13 +1,13 @@
 module Cat where
 
-import Cat.Categories.Sets
-import Cat.Categories.Cat
-import Cat.Categories.Rel
+import Cat.Cubical
+import Cat.Category
+import Cat.Functor
 import Cat.Category.Pathy
 import Cat.Category.Bij
 import Cat.Category.Free
 import Cat.Category.Properties
-import Cat.Category
-import Cat.Cubical
-import Cat.Functor
-import Cat.Naturality
+import Cat.Categories.Sets
+import Cat.Categories.Cat
+import Cat.Categories.Rel
+import Cat.Categories.Fun
diff --git a/src/Cat/Naturality.agda b/src/Cat/Categories/Fun.agda
similarity index 95%
rename from src/Cat/Naturality.agda
rename to src/Cat/Categories/Fun.agda
index c6ba91f..4be2d3d 100644
--- a/src/Cat/Naturality.agda
+++ b/src/Cat/Categories/Fun.agda
@@ -1,5 +1,5 @@
 {-# OPTIONS --allow-unsolved-metas #-}
-module Cat.Naturality where
+module Cat.Categories.Fun where
 
 open import Agda.Primitive
 open import Cubical
@@ -93,8 +93,9 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
       ; ident = λ {A B} → :ident: {A} {B}
       }
 
-  aCat : Category (ℓc ⊔ (ℓc' ⊔ (ℓd ⊔ ℓd'))) (ℓc ⊔ (ℓc' ⊔ ℓd'))
-  aCat = record
+  -- Functor categories. Objects are functors, arrows are natural transformations.
+  Fun : Category (ℓc ⊔ (ℓc' ⊔ (ℓd ⊔ ℓd'))) (ℓc ⊔ (ℓc' ⊔ ℓd'))
+  Fun = record
     { Object = Functor ℂ 𝔻
     ; Arrow = NaturalTranformation
     ; 𝟙 = λ {F} → identityNat F