links functors between categories

fredrik-bakke · Sep 17, 2023 · 47f04e3 · 47f04e3
1 parent 3987828
commit 47f04e3
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 3 deletions.
diff --git a/src/category-theory/functors-categories.lagda.md b/src/category-theory/functors-categories.lagda.md
@@ -19,8 +19,9 @@ open import foundation.universe-levels
 
 ## Idea
 
-A functor between two categories is a functor between the underlying
-precategories.
+A **functor** between two categories is a
+[functor](category-theory.functors-categories.md) between the underlying
+[categories](category-theory.categories.md).
 
 ## Definition
 

diff --git a/src/category-theory/functors-precategories.lagda.md b/src/category-theory/functors-precategories.lagda.md
@@ -22,7 +22,8 @@ open import foundation.universe-levels
 
 ## Idea
 
-A functor from a precategory `C` to a precategory `D` consists of:
+A **functor** from a [precategory](category-theory.precategories.md) `C` to a
+precategory `D` consists of:
 
 - a map `F₀ : C → D` on objects,
 - a map `F₁ : hom x y → hom (F₀ x) (F₀ y)` on morphisms, such that the following