modified the explanation of horizontal composition to better fit its …

…formal definition in the code, and also added some links

src/category-theory/monads-on-precategories.lagda.md

@@ -22,10 +22,12 @@ open import foundation-core.cartesian-product-types
 
 ## Idea
 
-A monad on a precategory `C` consists of an endofunctor `T : C → C` together
-with two natural transformations: `η : 1_C ⇒ T` and `μ : T² ⇒ T` (where
-`1_C : C → C` is the identity functor for `C`, and `T²` is the functor
-`T ∘ T : C → C`).
+A monad on a precategory `C` consists of an
+endo[functor](category-theory.functors-precategories.md) `T : C → C` together
+with two
+[natural transformations](category-theory.natural-transformations-functors-precategories.md):
+`η : 1_C ⇒ T` and `μ : T² ⇒ T` (where `1_C : C → C` is the identity functor for
+`C`, and `T²` is the functor `T ∘ T : C → C`).
 
 These must fulfill the _coherence conditions_:
 

src/category-theory/natural-transformations-functors-precategories.lagda.md

@@ -324,11 +324,14 @@ module _
 
 ## Horizontal composition
 
-Horizontal composition (here denoted by `*`) is generalized whiskering (here
-denoted by `•`), and also defined by it. Given natural transformations
+Horizontal composition (here denoted by `*`) is generalized
+[whiskering](category-theory.natural-transformations-functors-precategories.md#whiskering)
+(here denoted by `•`), and also defined by it. Given natural transformations
 `α : F ⇒ G`, `F, G : C → D`, and `β : H ⇒ I`, `H, I : D → E`, we can form a
-natural transformation `β * α : H ∘ F ⇒ I ∘ G`. Its componentat at `x` is
-`(β * α)(x) = (β • G)(x) ∘ (H • α)(x)`.
+natural transformation `β * α : H ∘ F ⇒ I ∘ G`.
+
+More precisely, `β * α = (β • G) ∘ (H • α)`, that is, we compose two natural
+transformations obtained by whiskering.
 
 ```agda
 module _