+ <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>.
+