-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>B</b>, <b>C</b>, <b>D</b>, and <b>E</b>. Let `F` be a functor from <b>B</b> to <b>C</b>; `G`, `H`, and `J` be functors from <b>C</b> to <b>D</b>; and `K` and `L` be functors from <b>D</b> to <b>E</b>. 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:
+
+<pre>
+ - <b>B</b> -+ +--- <b>C</b> --+ +---- <b>D</b> -----+ +-- <b>E</b> --
+ | | | | | |
+ F: ------> G: ------> K: ------>
+ | | | | | η | | | ψ
+ | | | | v | | v
+ | | H: ------> L: ------>
+ | | | | | φ | |
+ | | | | v | |
+ | | J: ------> | |
+ -----+ +--------+ +------------+ +-------
+</pre>
+
+Then <code>(η F)</code> is a natural transformation from the (composite) functor `GF` to the composite functor `HF`, such that where `B1` is an element of category <b>B</b>, <code>(η F)[B1] = η[F(B1)]</code>---that is, the morphism in <b>D</b> that <code>η</code> assigns to the element `F(B1)` of <b>C</b>.
+
+And <code>(K η)</code> is a natural transformation from the (composite) functor `KG` to the (composite) functor `KH`, such that where `C1` is an element of category <b>C</b>, <code>(K η)[C1] = K(η[C1])</code>---that is, the morphism in <b>E</b> that `K` assigns to the morphism <code>η[C1]</code> of <b>D</b>.
+
+
+<code>(φ -v- η)</code> is a natural transformation from `G` to `J`; this is known as a "vertical composition". For any morphism <code>f:C1→C2</code> in <b>C</b>:
+
+<pre>
+ φ[C2] ∘ H(f) ∘ η[C1] = φ[C2] ∘ H(f) ∘ η[C1]
+</pre>
+
+by naturalness of <code>φ</code>, is:
+
+<pre>
+ φ[C2] ∘ H(f) ∘ η[C1] = J(f) ∘ φ[C1] ∘ η[C1]
+</pre>
+
+by naturalness of <code>η</code>, is:
+
+<pre>
+ φ[C2] ∘ η[C2] ∘ G(f) = J(f) ∘ φ[C1] ∘ η[C1]
+</pre>
+
+Hence, we can define <code>(φ -v- η)[\_]</code> as: <code>φ[\_] ∘ η[\_]</code> and rely on it to satisfy the constraints for a natural transformation from `G` to `J`:
+
+<pre>
+ (φ -v- η)[C2] ∘ G(f) = J(f) ∘ (φ -v- η)[C1]
+</pre>
+
+An observation we'll rely on later: given the definitions of vertical composition and of how natural transformations compose with functors, it follows that:
+
+<pre>
+ ((φ -v- η) F) = ((φ F) -v- (η F))
+</pre>