-Consider four categories B,C,D, and E.
-Let F be a functor from B to C; G,H, and J be functors from C to D; and K and L be functors from D to E. Let eta be a natural transformation from G to H; phi be a natural transformation from H to J; and psi be a natural transformation from K to L. Pictorally:
-
-- B -+ +--- C --+ +---- D -----+ +-- E --
- | | | | | |
- F: ------> G: ------> K: ------>
- | | | | | eta | | | psi
- | | | | v | | v
- | | H: ------> L: ------>
- | | | | | phi | |
- | | | | v | |
- | | J: ------> | |
------+ +--------+ +------------+ +-------
-
-(eta F) is a natural transformation from the (composite) functor GF to the composite functor HF, such that where b1 is an element of category B, (eta F)[b1] = eta[F(b1)]---that is, the morphism in D that eta assigns to the element F(b1) of C.
-
-(K eta) is a natural transformation from the (composite) functor KG to the (composite) functor KH, such that where c1 is an element of category C, (K eta)[c1] = K(eta[c1])---that is, the morphism in E that K assigns to the morphism eta[c1] of D.
-
-
-(phi -v- eta) is a natural transformation from G to J; this is known as a "vertical composition". We will rely later on this:
- phi[c2] o H(f) o eta[c1] = phi[c2] o H(f) o eta[c1]
- -------------
- by naturalness of phi, is:
- --------------
- phi[c2] o H(f) o eta[c1] = J(f) o phi[c1] o eta[c1]
- --------------
- by naturalness of eta, is:
- --------------
- phi[c2] o eta[c2] o G(f) = J(f) o phi[c1] o eta[c1]
- ----------------- -----------------
-Hence, we can define (phi -v- eta)[c1] as: phi[c1] o eta[c1] and rely on it to satisfy the constraints for a natural transformation from G to J:
- ----------------- -----------------
- (phi -v- eta)[c2] o G(f) = J(f) o (phi -v- eta)[c1]
+Consider four categories **B**, **C**, **D**, and **E**. Let `F` be a functor from **B** to **C**; `G`, `H`, and `J` be functors from **C** to **D**; and `K` and `L` be functors from **D** to **E**. Let η be a natural transformation from `G` to `H`; φ be a natural transformation from `H` to `J`; and ψ be a natural transformation from `K` to `L`. Pictorally:
+
+ - **B** -+ +--- **C** --+ +---- **D** -----+ +-- **E** --
+ | | | | | |
+ F: ------> G: ------> K: ------>
+ | | | | | η | | | ψ
+ | | | | v | | v
+ | | H: ------> L: ------>
+ | | | | | φ | |
+ | | | | v | |
+ | | J: ------> | |
+ -----+ +--------+ +------------+ +-------
+
+Then `(η F)` is a natural transformation from the (composite) functor `GF` to the composite functor `HF`, such that where `b1` is an element of category **B**, `(η F)[b1] = η[F(b1)]`---that is, the morphism in **D** that η assigns to the element `F(b1)` of **C**.
+
+And `(K η)` is a natural transformation from the (composite) functor `KG` to the (composite) functor `KH`, such that where `C1` is an element of category **C**, `(K η)[C1] = K(η[C1])`---that is, the morphism in **E** that `K` assigns to the morphism η[C1]` of **D**.
+
+
+`(φ -v- η)` is a natural transformation from `G` to `J`; this is known as a "vertical composition". We will rely later on this, where `f:C1->C2`:
+
+ φ[C2] o H(f) o η[C1] = φ[C2] o H(f) o η[C1]
+
+by naturalness of φ, is:
+
+ φ[C2] o H(f) o η[C1] = J(f) o φ[C1] o η[C1]
+
+by naturalness of η, is:
+
+ φ[C2] o η[C2] o G(f) = J(f) o φ[C1] o η[C1]
+
+Hence, we can define `(φ -v- η)[x]` as: φ[x] o η[x]` and rely on it to satisfy the constraints for a natural transformation from `G` to `J`:
+
+ (φ -v- η)[C2] o G(f) = J(f) o (φ -v- η)[C1]
+
+An observation we'll rely on later: given the definitions of vertical composition and of how natural transformations compose with functors, it follows that:
+
+ ((φ -v- η) F) = ((φ F) -v- (η F))