-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]
+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))