- q = (p Q)
- = ((p <=< unit) Q)
- = (((join P') -v- (M p) -v- unit) Q)
- = ((join P'Q) -v- ((M p) Q) -v- (unit Q))
- = ((join P'Q) -v- (M (p Q)) -v- (unit Q))
- ??
- = q <=< (unit Q)
+<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>
+
+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 `MR'`, and <code>γ</code> is <code>(ρ G)</code>, that is, a natural transformation from `G` to `MR'G`, then we can extend (iii.2) as follows:
+
+<pre>
+ γ = (ρ G)
+ = ((ρ <=< unit) G)
+ = (((join R') -v- (M ρ) -v- unit) G)
+ = (((join R') G) -v- ((M ρ) G) -v- (unit G))
+ = ((join (R'G)) -v- (M (ρ G)) -v- (unit G))
+ since γ = (ρ G) is a natural transformation to MR'G,
+ this satisfies the definition <=<:
+ = γ <=< (unit G)
+</pre>
+
+where as we said <code>γ</code> is a natural transformation from `G` to some `MR'G`.