-That's it. (Well, perhaps we're cheating a bit, because `q <=< p` isn't fully defined on `T`, but only when `P` is a functor to `MP'` and `Q` is a functor from `P'`. But wherever `<=<` is defined, the monoid laws are satisfied:
+ (iii.2) ρ = ρ <=< unit
+ (here ρ has to be a natural transformation from 1C)
+</pre>
+
+If <code>φ</code> is a natural transformation from `F` to `M(1C)` and <code>γ</code> is <code>(φ G')</code>, that is, a natural transformation from `FG'` to `MG'`, then we can extend (iii.1) as follows:
+
+<pre>
+ γ = (φ G')
+ = ((unit <=< φ) G')
+ = (((join 1C) -v- (M unit) -v- φ) G')
+ = (((join 1C) G') -v- ((M unit) G') -v- (φ G'))
+ = ((join (1C G')) -v- (M (unit G')) -v- γ)
+ = ((join G') -v- (M (unit G')) -v- γ)
+ since (unit G') is a natural transformation to MG',
+ this satisfies the definition for <=<:
+ = (unit G') <=< γ
+</pre>