functors _between_ categories

fredrik-bakke · Sep 21, 2023 · 5577dbb · 5577dbb
1 parent 786664f
commit 5577dbb
Show file tree

Hide file tree

Showing 10 changed files with 15 additions and 15 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -1,4 +1,4 @@
-# Representable functors on precategories
+# Representable functors between precategories
 
 ```agda
 module category-theory.representable-functors-precategories where