In the first, `P` has become `int` and `Q` has become `bool`. (The boxed type <code><u>Q</u></code> is <code><u>bool</u></code>).
Note that the left-hand schema `P` is permitted to itself be a boxed type. That is, where
-if `α list` is our box type, we can write the second arrow as
+if `α list` is our box type, we can write the second type as:
<code><u>int</u> -> <u>int list</u></code>
<code><=< or mcomp : (Q -> <u>R</u>) -> (P -> <u>Q</u>) -> (P -> <u>R</u>)</code>
-<code>>=> or mpmoc (flip mcomp): (P -> <u>Q</u>) -> (Q -> <u>R</u>) -> (P -> <u>R</u>)</code>
+<code>>=> (flip mcomp, should we call it mpmoc?): (P -> <u>Q</u>) -> (Q -> <u>R</u>) -> (P -> <u>R</u>)</code>
<code>>>= or mbind : (<u>Q</u>) -> (Q -> <u>R</u>) -> (<u>R</u>)</code>
-<code>=<< or mdnib (flip mbind) (<u>Q</u>) -> (Q -> <u>R</u>) -> (<u>R</u>)</code>
+<code>=<< (flip mbind, should we call it mdnib?) (Q -> <u>R</u>) -> (<u>Q</u>) -> (<u>R</u>)</code>
<code>join: <span class="box2">P</span> -> <u>P</u></code>
if there is a `map` function defined for that box type with the type given above. This
has to obey the following Map Laws:
- TODO LAWS
+ <code>map (id : α -> α) = (id : <u>α</u> -> <u>α</u>)</code>
+ <code>map (g ○ f) = (map g) ○ (map f)</code>
+
+ Essentially these say that `map` is a homomorphism from `(α -> β, ○, id)` to <code>(<u>α</u> -> <u>β</u>, ○', id')</code>, where `○'` and `id'` are `○` and `id` restricted to arguments of type <code><u>_</u></code>.
+
* ***MapNable*** (in Haskelese, "Applicatives") A Mappable box type is *MapNable*
if there are in addition `map2`, `mid`, and `mapply`. (Given either