+That's it. Well, there may be a wrinkle here. I don't know whether the definition of a monoid requires the operation to be defined for every pair in its set. In the present case, <code>γ <=< φ</code> isn't fully defined on `T`, but only when <code>φ</code> is a transformation to some `MF'` and <code>γ</code> is a transformation from `F'`. But wherever `<=<` is defined, the monoid laws are satisfied:
+
+<pre>
+ (i) γ `<=<` φ is also in T
+
+ (ii) (ρ `<=<` γ) `<=<` φ = ρ `<=<` (γ `<=<` φ)
+
+ (iii.1) unit `<=<` φ = φ (here φ has to be a natural transformation to M(1C))
+
+ (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 -v- (M unit) -v- φ) G')
+ = (join G') -v- ((M unit) G') -v- (φ G')
+ = (join G') -v- (M (unit G')) -v- γ
+ ??
+ = (unit G') `<=<` γ
+</pre>
+
+where as we said <code>γ</code> is a natural transformation from some `FG'` to `MG'`.
+
+Similarly, if <code>φ</code> is a natural transformation from `1C` to `MF'`, and <code>γ</code> is <code>(φ G)</code>, that is, a natural transformation from `G` to `MF'G`, then we can extend (iii.2) as follows: