links functors between categories

Author: fredrik-bakke

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
 

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