diff --git a/src/category-theory/anafunctors-categories.lagda.md b/src/category-theory/anafunctors-categories.lagda.md
index d6d91c5f3f..4cc6b74fba 100644
--- a/src/category-theory/anafunctors-categories.lagda.md
+++ b/src/category-theory/anafunctors-categories.lagda.md
@@ -1,4 +1,4 @@
-# Anafunctors on categories
+# Anafunctors between categories
 
 ```agda
 module category-theory.anafunctors-categories where
diff --git a/src/category-theory/anafunctors-precategories.lagda.md b/src/category-theory/anafunctors-precategories.lagda.md
index ef565f5cd5..929d1577f4 100644
--- a/src/category-theory/anafunctors-precategories.lagda.md
+++ b/src/category-theory/anafunctors-precategories.lagda.md
@@ -1,4 +1,4 @@
-# Anafunctors on precategories
+# Anafunctors between precategories
 
 ```agda
 module category-theory.anafunctors-precategories where
diff --git a/src/category-theory/functors-categories.lagda.md b/src/category-theory/functors-categories.lagda.md
index b8aa0019a8..f2b3cea5fd 100644
--- a/src/category-theory/functors-categories.lagda.md
+++ b/src/category-theory/functors-categories.lagda.md
@@ -1,4 +1,4 @@
-# Functors on categories
+# functors between categories
 
 ```agda
 module category-theory.functors-categories where
@@ -105,7 +105,7 @@ module _
       ( F)
 ```
 
-### Functors on categories
+### functors between categories
 
 ```agda
 module _
@@ -251,7 +251,7 @@ module _
       ( F)
 ```
 
-### Extensionality of functors on categories
+### Extensionality of functors between categories
 
 ```agda
 module _
diff --git a/src/category-theory/functors-precategories.lagda.md b/src/category-theory/functors-precategories.lagda.md
index d8e1cb3c6b..8d0dbecfbc 100644
--- a/src/category-theory/functors-precategories.lagda.md
+++ b/src/category-theory/functors-precategories.lagda.md
@@ -1,4 +1,4 @@
-# Functors on precategories
+# functors between precategories
 
 ```agda
 module category-theory.functors-precategories where
@@ -110,7 +110,7 @@ module _
   preserves-id-hom-is-functor-map-Precategory = pr2
 ```
 
-### Functors on Precategories
+### functors between precategories
 
 ```agda
 module _
@@ -276,7 +276,7 @@ module _
   pr2 is-functor-map-Precategory-Prop = is-prop-is-functor-map-Precategory
 ```
 
-### Extensionality of functors on precategories
+### Extensionality of functors between precategories
 
 ```agda
 module _
diff --git a/src/category-theory/natural-isomorphisms-categories.lagda.md b/src/category-theory/natural-isomorphisms-categories.lagda.md
index da1971bf14..de8b1ddd2c 100644
--- a/src/category-theory/natural-isomorphisms-categories.lagda.md
+++ b/src/category-theory/natural-isomorphisms-categories.lagda.md
@@ -1,4 +1,4 @@
-# Natural isomorphisms between functors on categories
+# Natural isomorphisms between functors between categories
 
 ```agda
 module category-theory.natural-isomorphisms-categories where
diff --git a/src/category-theory/natural-isomorphisms-precategories.lagda.md b/src/category-theory/natural-isomorphisms-precategories.lagda.md
index 1071ab78eb..9f300e1cfa 100644
--- a/src/category-theory/natural-isomorphisms-precategories.lagda.md
+++ b/src/category-theory/natural-isomorphisms-precategories.lagda.md
@@ -1,4 +1,4 @@
-# Natural isomorphisms between functors on precategories
+# Natural isomorphisms between functors between precategories
 
 ```agda
 module category-theory.natural-isomorphisms-precategories where
diff --git a/src/category-theory/natural-transformations-categories.lagda.md b/src/category-theory/natural-transformations-categories.lagda.md
index 3bd4983363..1e1c7bfbe3 100644
--- a/src/category-theory/natural-transformations-categories.lagda.md
+++ b/src/category-theory/natural-transformations-categories.lagda.md
@@ -1,4 +1,4 @@
-# Natural transformations between functors on categories
+# Natural transformations between functors between categories
 
 ```agda
 module category-theory.natural-transformations-categories where
@@ -25,7 +25,7 @@ open import foundation.universe-levels
 ## Idea
 
 A **natural transformation** between
-[functors on categories](category-theory.functors-categories.md) is a
+[functors between categories](category-theory.functors-categories.md) is a
 [natural transformation](category-theory.natural-transformations-precategories.md)
 between the [functors](category-theory.functors-precategories.md) on the
 underlying [precategories](category-theory.precategories.md).
diff --git a/src/category-theory/natural-transformations-precategories.lagda.md b/src/category-theory/natural-transformations-precategories.lagda.md
index 659d7749d6..b10480f3b6 100644
--- a/src/category-theory/natural-transformations-precategories.lagda.md
+++ b/src/category-theory/natural-transformations-precategories.lagda.md
@@ -1,4 +1,4 @@
-# Natural transformations between functors on precategories
+# Natural transformations between functors between precategories
 
 ```agda
 module category-theory.natural-transformations-precategories where
diff --git a/src/category-theory/representable-functors-categories.lagda.md b/src/category-theory/representable-functors-categories.lagda.md
index 18c36b73e5..ee6390e5d5 100644
--- a/src/category-theory/representable-functors-categories.lagda.md
+++ b/src/category-theory/representable-functors-categories.lagda.md
@@ -1,4 +1,4 @@
-# Representable functors on categories
+# Representable functors between categories
 
 ```agda
 module category-theory.representable-functors-categories where
diff --git a/src/category-theory/representable-functors-precategories.lagda.md b/src/category-theory/representable-functors-precategories.lagda.md
index 159efaebbe..6015906898 100644
--- a/src/category-theory/representable-functors-precategories.lagda.md
+++ b/src/category-theory/representable-functors-precategories.lagda.md
@@ -1,4 +1,4 @@
-# Representable functors on precategories
+# Representable functors between precategories
 
 ```agda
 module category-theory.representable-functors-precategories where