+<pre>
+ (ii) (ρ <=< γ) <=< φ = ρ <=< (γ <=< φ)
+ ==>
+ (ρ <=< γ) is a transformation from G to MR', so
+ (ρ <=< γ) <=< φ becomes: ((join R') (M (ρ <=< γ)) φ)
+ which is: ((join R') (M ((join R') (M ρ) γ)) φ)
+
+ similarly, ρ <=< (γ <=< φ) is:
+ ((join R') (M ρ) ((join G') (M γ) φ))
+
+ substituting these into (ii), and helping ourselves to associativity on the rhs, we get:
+ ((join R') (M ((join R') (M ρ) γ)) φ) = ((join R') (M ρ) (join G') (M γ) φ)
+
+ which by the distributivity of functors over composition, and helping ourselves to associativity on the lhs, yields:
+ ((join R') (M join R') (MM ρ) (M γ) φ) = ((join R') (M ρ) (join G') (M γ) φ)
+
+ which by lemma 1, with ρ a transformation from G' to MR', yields:
+ ((join R') (M join R') (MM ρ) (M γ) φ) = ((join R') (join MR') (MM ρ) (M γ) φ)
+
+ [-- Are the next two steps too cavalier? --]
+
+ which will be true for all ρ, γ, φ only when:
+ ((join R') (M join R')) = ((join R') (join MR')), for any R'
+
+ which will in turn be true when:
+ (ii') (join (M join)) = (join (join M))
+</pre>
+
+<pre>
+ (iii.1) (unit G') <=< γ = γ
+ when γ is a natural transformation from some FG' to MG'
+ ==>
+ (unit G') is a transformation from G' to MG', so:
+ (unit G') <=< γ becomes: ((join G') (M (unit G')) γ)
+ which is: ((join G') ((M unit) G') γ)
+
+ substituting in (iii.1), we get:
+ ((join G') ((M unit) G') γ) = γ