Since composition is associative I don't specify the order of composition on the rhs.
-In other words, `<=<` is a binary operator that takes us from two members <code>φ</code> and <code>γ</code> of `T` to a composite natural transformation. (In functional programming, at least, this is called the "Kleisli composition operator". Sometimes it's written <code>φ >=> γ</code> where that's the same as <code>γ <=< φ</code>.)
+In other words, `<=<` is a binary operator that takes us from two members <code>φ</code> and <code>γ</code> of `T` to a composite natural transformation. (In functional programming, at least, this is called the "Kleisli composition operator". Sometimes it's written <code>φ >=> γ</code> where that's the same as <code>γ <=< φ</code>.)
-<code>φ</code> is a transformation from `F` to `MF'`, where the latter = `MG`; <code>(M γ)</code> is a transformation from `MG` to `MMG'`; and `(join G')` is a transformation from `MMG'` to `MG'`. So the composite <code>γ <=< φ</code> will be a transformation from `F` to `MG'`, and so also eligible to be a member of `T`.
+<code>φ</code> is a transformation from `F` to `MF'`, where the latter = `MG`; <code>(M γ)</code> is a transformation from `MG` to `MMG'`; and `(join G')` is a transformation from `MMG'` to `MG'`. So the composite <code>γ <=< φ</code> will be a transformation from `F` to `MG'`, and so also eligible to be a member of `T`.
Now we can specify the "monad laws" governing a monad as follows:
(T, <=<, unit) constitute a monoid
-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:
+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
+ (i) γ <=< φ is also in T
- (ii) (ρ `<=<` γ) `<=<` φ = ρ `<=<` (γ `<=<` φ)
+ (ii) (ρ <=< γ) <=< φ = ρ <=< (γ <=< φ)
- (iii.1) unit `<=<` φ = φ (here φ has to be a natural transformation to M(1C))
+ (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)
+ (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')
+ = ((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') <=< γ
</pre>
where as we said <code>γ</code> is a natural transformation from some `FG'` to `MG'`.
<pre>
γ = (φ G)
- = ((φ `<=<` unit) G)
+ = ((φ <=< unit) G)
= (((join F') -v- (M φ) -v- unit) G)
= ((join F'G) -v- ((M φ) G) -v- (unit G))
= ((join F'G) -v- (M (φ G)) -v- (unit G))
??
- = γ `<=<` (unit G)
+ = γ <=< (unit G)
</pre>
where as we said <code>γ</code> is a natural transformation from `G` to some `MF'G`.
</pre>
-Finally, we substitute <code>((join G') -v- (M γ) -v- φ)</code> for <code>γ <=< φ</code> in the monad laws. For simplicity, I'll omit the "-v-".
+Finally, we substitute <code>((join G') -v- (M γ) -v- φ)</code> for <code>γ <=< φ</code> in the monad laws. For simplicity, I'll omit the "-v-".
<pre>
for all φ,γ,ρ in T, where φ is a transformation from F to MF', γ is a transformation from G to MG', R is a transformation from R to MR', and F'=G and G'=R: