`F(g ∘ f) = F(g) ∘ F(f)`

-* if `η`

is a natural transformation from `F` to `G`, then for every `f:C1→C2`

in `F` and `G`'s source category `η[C2] ∘ F(f) = G(f) ∘ η[C1]`

.
+* if `η`

is a natural transformation from `G` to `H`, then for every `f:C1→C2`

in `G` and `H`'s source category `η[C2] ∘ G(f) = H(f) ∘ η[C1]`

.
+
+* `(η F)[E] = η[F(E)]`

+
+* `(K η)[E} = K(η[E])`

+
+* `((φ -v- η) F) = ((φ F) -v- (η F))`

Let's use the definitions of naturalness, and of composition of natural transformations, to establish two lemmas.
-Recall that join is a natural transformation from the (composite) functor `MM` to `M`. So for elements `C1` in `f:C1→C2`

in `f:C1→C2`

in (1) join[C2] ∘ MM(f) = M(f) ∘ join[C1]-Next, consider the composite transformation

`((join MG') -v- (MM γ))`

.
+Next, let `γ`

be a transformation from `G` to `MG'`, and
+ consider the composite transformation `((join MG') -v- (MM γ))`

.
-* `γ`

is a transformation from `G` to `MG'`, and assigns elements `C1` in `γ\*: G(C1) → MG'(C1)`

. `(MM γ)`

is a transformation that instead assigns `C1` the morphism `MM(γ\*)`

.
+* `γ`

assigns elements `C1` in `γ\*: G(C1) → MG'(C1)`

. `(MM γ)`

is a transformation that instead assigns `C1` the morphism `MM(γ\*)`

.
-* `(join MG')` is a transformation from `MMMG'` to `MMG'` that assigns `C1` the morphism `join[MG'(C1)]`.
+* `(join MG')` is a transformation from `MM(MG')` to `M(MG')` that assigns `C1` the morphism `join[MG'(C1)]`.
Composing them:
@@ -311,17 +318,17 @@ Composing them:
(2) ((join MG') -v- (MM γ)) assigns to C1 the morphism join[MG'(C1)] ∘ MM(γ*).
-Next, consider the composite transformation `((M γ) -v- (join G))`

.
+Next:
```
- (3) This assigns to C1 the morphism M(γ*) ∘ join[G(C1)].
+ (3) Consider the composite transformation
````((M γ) -v- (join G))`

. This assigns to C1 the morphism M(γ*) ∘ join[G(C1)].

So for every element `C1` of ((join MG') -v- (MM γ))[C1], by (2) is: - join[MG'(C1)] ∘ MM(γ*), which by (1), with f=γ*: G(C1)→MG'(C1) is: + join[MG'(C1)] ∘ MM(γ*), which by (1), with f=γ*:G(C1)→MG'(C1) is: M(γ*) ∘ join[G(C1)], which by 3 is: ((M γ) -v- (join G))[C1]@@ -329,33 +336,34 @@ So for every element `C1` of

- ((join MG') -v- (MM γ)) = ((M γ) -v- (join G)), where γ is a transformation from G to MG'. + ((join MG') -v- (MM γ)) = ((M γ) -v- (join G)), + where as we said γ is a natural transformation from G to MG'.-Next recall that unit is a natural transformation from `1C` to `M`. So for elements `C1` in

`f:a→b`

in `f:C1→C2`

in - (4) unit[b] ∘ f = M(f) ∘ unit[a] + (4) unit[C2] ∘ f = M(f) ∘ unit[C1]-Next consider the composite transformation

`((M γ) -v- (unit G))`

:
+Next:
- (5) This assigns to C1 the morphism M(γ*) ∘ unit[G(C1)]. + (5) Consider the composite transformation ((M γ) -v- (unit G)). This assigns to C1 the morphism M(γ*) ∘ unit[G(C1)].-Next consider the composite transformation

`((unit MG') -v- γ)`

.
+Next:
- (6) This assigns to C1 the morphism unit[MG'(C1)] ∘ γ*. + (6) Consider the composite transformation ((unit MG') -v- γ). This assigns to C1 the morphism unit[MG'(C1)] ∘ γ*.So for every element C1 of

((M γ) -v- (unit G))[C1], by (5) = - M(γ*) ∘ unit[G(C1)], which by (4), with f=γ*: G(C1)→MG'(C1) is: + M(γ*) ∘ unit[G(C1)], which by (4), with f=γ*:G(C1)→MG'(C1) is: unit[MG'(C1)] ∘ γ*, which by (6) = ((unit MG') -v- γ)[C1]@@ -363,7 +371,8 @@ So for every element C1 of

- (((M γ) -v- (unit G)) = ((unit MG') -v- γ)), where γ is a transformation from G to MG'. + (((M γ) -v- (unit G)) = ((unit MG') -v- γ)), + where as we said γ is a natural transformation from G to MG'.-- 2.11.0