- q = (p Q')
- = ((unit <=< p) Q')
- = ((join -v- (M unit) -v- p) Q')
- = (join Q') -v- ((M unit) Q') -v- (p Q')
- = (join Q') -v- (M (unit Q')) -v- q
+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- γ