- = ((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') `<=<` γ
+ = ((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') <=< γ