-Recall that join is a natural transformation from the (composite) functor MM to M. So for elements C1 in **C**, join[C1] will be a morphism from MM(C1) to M(C1). And for any morphism f:a->b in **C**:
+Recall that `join` is a natural transformation from the (composite) functor `MM` to `M`. So for elements `C1` in <b>C</b>, `join[C1]` will be a morphism from `MM(C1)` to `M(C1)`. And for any morphism <code>f:C1→C2</code> in <b>C</b>:
+
+<pre>
+ (1) join[C2] ∘ MM(f) = M(f) ∘ join[C1]
+</pre>
+
+Next, let <code>γ</code> be a transformation from `G` to `MG'`, and
+ consider the composite transformation <code>((join MG') -v- (MM γ))</code>.
+
+* <code>γ</code> assigns elements `C1` in <b>C</b> a morphism <code>γ\*:G(C1) → MG'(C1)</code>. <code>(MM γ)</code> is a transformation that instead assigns `C1` the morphism <code>MM(γ\*)</code>.
+
+* `(join MG')` is a transformation from `MM(MG')` to `M(MG')` that assigns `C1` the morphism `join[MG'(C1)]`.
+
+Composing them:
+
+<pre>
+ (2) ((join MG') -v- (MM γ)) assigns to C1 the morphism join[MG'(C1)] ∘ MM(γ*).
+</pre>
+
+Next, consider the composite transformation <code>((M γ) -v- (join G))</code>:
+
+<pre>
+ (3) ((M γ) -v- (join G)) assigns to C1 the morphism M(γ*) ∘ join[G(C1)].
+</pre>