- mcomp (mcomp j k) l (that is, (j <=< k) <=< l) = mcomp j (mcomp k l)
- mcomp mid k (that is, mid <=< k) = k
- mcomp k mid (that is, k <=< mid) = k
+ mcomp (mcomp j k) l (that is, (j <=< k) <=< l) == mcomp j (mcomp k l)
+ mcomp mid k (that is, mid <=< k) == k
+ mcomp k mid (that is, k <=< mid) == k
+
+ You could just as well express the Monad laws using `>=>`:
+
+ l >=> (k >=> j) == (l >=> k) >-> j
+ k >=> mid == k
+ mid >=> k == k
+
+ If you have any of `mcomp`, `mpmoc`, `mbind`, or `join`, you can use them to define the others. Also, with these functions you can define `m$` and `map2` from *MapNables*. So with Monads, all you really need to get the whole system of functions are a definition of `mid`, on the one hand, and one of `mcomp`, `mbind`, or `join`, on the other.
+
+ In practice, you will often work with `>>=`. In the Haskell manuals, they express the Monad Laws using `>>=` instead of the composition operators. This looks similar, but doesn't have the same symmetry:
+
+ u >>= (\a -> k a >>= j) == (u >>= k) >>= j
+ u >>= mid == u
+ mid a >>= k == k a
+
+ Also, Haskell calls `mid` `return` or `pure`, but we've stuck to our terminology in this context.
+
+ > <small>In Category Theory discussion, the Monad Laws are instead expressed in terms of `join` (which they call `μ`) and `mid` (which they call `η`). These are assumed to be "natural transformations" for their box type, which means that they satisfy these equations with that box type's `map`:
+ > <pre>map f ○ mid == mid ○ f<br>map f ○ join == join ○ map (map f)</pre>
+ > The Monad Laws then take the form:
+ > <pre>join ○ (map join) == join ○ join<br>join ○ mid == id == join ○ map mid</pre>
+ > Or, as the Category Theorist would state it, where `M` is the endofunctor that takes us from type `α` to type <code><u>α</u></code>:
+ > <pre>μ ○ M(μ) == μ ○ μ<br>μ ○ η = id == μ ○ M(η)</pre></small>