(iii.1) (unit G') <=< γ = γ
when γ is a natural transformation from some FG' to MG'
- (iii.2) γ = γ <=< (unit G)
+ (iii.2) γ = γ <=< (unit G)
when γ is a natural transformation from G to some MR'G
</pre>
-The standard category-theory presentation of the monad laws
------------------------------------------------------------
+Getting to the standard category-theory presentation of the monad laws
+----------------------------------------------------------------------
In category theory, the monad laws are usually stated in terms of `unit` and `join` instead of `unit` and `<=<`.
<!--
* functors "distribute over composition", that is for any morphisms `f` and `g` in `F`'s source category: <code>F(g ∘ f) = F(g) ∘ F(f)</code>
-* if <code>η</code> is a natural transformation from `F` to `G`, then for every <code>f:C1→C2</code> in `F` and `G`'s source category <b>C</b>: <code>η[C2] ∘ F(f) = G(f) ∘ η[C1]</code>.
+* if <code>η</code> is a natural transformation from `G` to `H`, then for every <code>f:C1→C2</code> in `G` and `H`'s source category <b>C</b>: <code>η[C2] ∘ G(f) = H(f) ∘ η[C1]</code>.
+
+* <code>(η F)[E] = η[F(E)]</code>
+
+* <code>(K η)[E} = K(η[E])</code>
+
+* <code>((φ -v- η) F) = ((φ F) -v- (η F))</code>
Let's use the definitions of naturalness, and of composition of natural transformations, to establish two lemmas.
-Recall that join is a natural transformation from the (composite) functor `MM` to `M`. So for elements `C1` in <b>C</b>, `join[C1]` will be a morphism from `MM(C1)` to `M(C1)`. And for any morphism <code>f:C1→C2</code> in <b>C</b>:
+Recall that `join` is a natural transformation from the (composite) functor `MM` to `M`. So for elements `C1` in <b>C</b>, `join[C1]` will be a morphism from `MM(C1)` to `M(C1)`. And for any morphism <code>f:C1→C2</code> in <b>C</b>:
<pre>
(1) join[C2] ∘ MM(f) = M(f) ∘ join[C1]
</pre>
-Next, consider the composite transformation <code>((join MG') -v- (MM γ))</code>.
+Next, let <code>γ</code> be a transformation from `G` to `MG'`, and
+ consider the composite transformation <code>((join MG') -v- (MM γ))</code>.
-* <code>γ</code> is a transformation from `G` to `MG'`, and assigns elements `C1` in <b>C</b> a morphism <code>γ\*: G(C1) → MG'(C1)</code>. <code>(MM γ)</code> is a transformation that instead assigns `C1` the morphism <code>MM(γ\*)</code>.
+* <code>γ</code> assigns elements `C1` in <b>C</b> a morphism <code>γ\*:G(C1) → MG'(C1)</code>. <code>(MM γ)</code> is a transformation that instead assigns `C1` the morphism <code>MM(γ\*)</code>.
-* `(join MG')` is a transformation from `MMMG'` to `MMG'` that assigns `C1` the morphism `join[MG'(C1)]`.
+* `(join MG')` is a transformation from `MM(MG')` to `M(MG')` that assigns `C1` the morphism `join[MG'(C1)]`.
Composing them:
(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>.
+Next, consider the composite transformation <code>((M γ) -v- (join G))</code>:
<pre>
- (3) This assigns to C1 the morphism M(γ*) ∘ join[G(C1)].
+ (3) ((M γ) -v- (join G)) assigns to C1 the morphism M(γ*) ∘ join[G(C1)].
</pre>
So for every element `C1` of <b>C</b>:
<pre>
((join MG') -v- (MM γ))[C1], by (2) is:
- join[MG'(C1)] ∘ MM(γ*), which by (1), with f=γ*: G(C1)→MG'(C1) is:
+ join[MG'(C1)] ∘ MM(γ*), which by (1), with f=γ*:G(C1)→MG'(C1) is:
M(γ*) ∘ join[G(C1)], which by 3 is:
((M γ) -v- (join G))[C1]
</pre>
So our **(lemma 1)** is:
<pre>
- ((join MG') -v- (MM γ)) = ((M γ) -v- (join G)), where γ is a transformation from G to MG'.
+ ((join MG') -v- (MM γ)) = ((M γ) -v- (join G)),
+ where as we said γ is a natural transformation from G to MG'.
</pre>
-Next recall that unit is a natural transformation from `1C` to `M`. So for elements `C1` in <b>C</b>, `unit[C1]` will be a morphism from `C1` to `M(C1)`. And for any morphism <code>f:a→b</code> in <b>C</b>:
+Next recall that `unit` is a natural transformation from `1C` to `M`. So for elements `C1` in <b>C</b>, `unit[C1]` will be a morphism from `C1` to `M(C1)`. And for any morphism <code>f:C1→C2</code> in <b>C</b>:
<pre>
- (4) unit[b] ∘ f = M(f) ∘ unit[a]
+ (4) unit[C2] ∘ f = M(f) ∘ unit[C1]
</pre>
-Next consider the composite transformation <code>((M γ) -v- (unit G))</code>:
+Next, consider the composite transformation <code>((M γ) -v- (unit G))</code>:
<pre>
- (5) This assigns to C1 the morphism M(γ*) ∘ unit[G(C1)].
+ (5) ((M γ) -v- (unit G)) assigns to C1 the morphism M(γ*) ∘ unit[G(C1)].
</pre>
-Next consider the composite transformation <code>((unit MG') -v- γ)</code>.
+Next, consider the composite transformation <code>((unit MG') -v- γ)</code>:
<pre>
- (6) This assigns to C1 the morphism unit[MG'(C1)] ∘ γ*.
+ (6) ((unit MG') -v- γ) assigns to C1 the morphism unit[MG'(C1)] ∘ γ*.
</pre>
So for every element C1 of <b>C</b>:
<pre>
((M γ) -v- (unit G))[C1], by (5) =
- M(γ*) ∘ unit[G(C1)], which by (4), with f=γ*: G(C1)→MG'(C1) is:
+ M(γ*) ∘ unit[G(C1)], which by (4), with f=γ*:G(C1)→MG'(C1) is:
unit[MG'(C1)] ∘ γ*, which by (6) =
((unit MG') -v- γ)[C1]
</pre>
So our **(lemma 2)** is:
<pre>
- (((M γ) -v- (unit G)) = ((unit MG') -v- γ)), where γ is a transformation from G to MG'.
+ (((M γ) -v- (unit G)) = ((unit MG') -v- γ)),
+ where as we said γ is a natural transformation from G to MG'.
</pre>
-7. The functional programming presentation of the monad laws
-------------------------------------------------------------
+Getting to the functional programming presentation of the monad laws
+--------------------------------------------------------------------
In functional programming, unit is usually called "return" and the monad laws are usually stated in terms of return and an operation called "bind" which is interdefinable with <=< or with join.
Additionally, whereas in category-theory one works "monomorphically", in functional programming one usually works with "polymorphic" functions.