= (((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 <=<:
+ since (unit G') is a natural transformation to MG',
+ this satisfies the definition for <=<:
= (unit G') <=< γ
</pre>
= (((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 for <=<:
+ since γ = (ρ G) is a natural transformation to MR'G,
+ this satisfies the definition <=<:
= γ <=< (unit G)
</pre>