Now we can specify the "monad laws" governing a monad as follows:
+<pre>
(T, <=<, unit) constitute a monoid
+</pre>
+
+That's it. Well, there may be a wrinkle here.
-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:
+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
Composing them:
<pre>
- (2) <code>((join MG') -v- (MM γ))</code> assigns to `C1` the morphism <code>join[MG'(C1)] ∘ MM(γ*)</code>.
+ (2) ((join MG') -v- (MM γ)) assigns to `C1` the morphism join[MG'(C1)] ∘ MM(γ*).
</pre>
Next, consider the composite transformation <code>((M γ) -v- (join G))</code>.
</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: