cat theory tweaks
authorJim Pryor <profjim@jimpryor.net>
Tue, 2 Nov 2010 15:39:13 +0000 (11:39 -0400)
committerJim Pryor <profjim@jimpryor.net>
Tue, 2 Nov 2010 15:39:13 +0000 (11:39 -0400)
Signed-off-by: Jim Pryor <profjim@jimpryor.net>
advanced_topics/monads_in_category_theory.mdwn

index f05747f..0c60f2e 100644 (file)
@@ -273,8 +273,8 @@ Summarizing then, the monad laws can be expressed as:
 
 
 
-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 `<=<`.
 
 <!--
@@ -308,7 +308,7 @@ Recall that `join` is a natural transformation from the (composite) functor `MM`
 Next, let <code>&gamma;</code> be a transformation from `G` to `MG'`, and
  consider the composite transformation <code>((join MG') -v- (MM &gamma;))</code>.
 
-*      <code>&gamma;</code> assigns elements `C1` in <b>C</b> a morphism <code>&gamma;\*: G(C1) &rarr; MG'(C1)</code>. <code>(MM &gamma;)</code> is a transformation that instead assigns `C1` the morphism <code>MM(&gamma;\*)</code>.
+*      <code>&gamma;</code> assigns elements `C1` in <b>C</b> a morphism <code>&gamma;\*:G(C1) &rarr; MG'(C1)</code>. <code>(MM &gamma;)</code> is a transformation that instead assigns `C1` the morphism <code>MM(&gamma;\*)</code>.
 
 *      `(join MG')` is a transformation from `MM(MG')` to `M(MG')` that assigns `C1` the morphism `join[MG'(C1)]`.
 
@@ -318,10 +318,10 @@ Composing them:
        (2) ((join MG') -v- (MM &gamma;)) assigns to C1 the morphism join[MG'(C1)] &#8728; MM(&gamma;*).
 </pre>
 
-Next:
+Next, consider the composite transformation <code>((M &gamma;) -v- (join G))</code>:
 
 <pre>
-       (3) Consider the composite transformation <code>((M &gamma;) -v- (join G))</code>. This assigns to C1 the morphism M(&gamma;*) &#8728; join[G(C1)].
+       (3) ((M &gamma;) -v- (join G)) assigns to C1 the morphism M(&gamma;*) &#8728; join[G(C1)].
 </pre>
 
 So for every element `C1` of <b>C</b>:
@@ -347,16 +347,16 @@ Next recall that `unit` is a natural transformation from `1C` to `M`. So for ele
        (4) unit[C2] &#8728; f = M(f) &#8728; unit[C1]
 </pre>
 
-Next:
+Next, consider the composite transformation <code>((M &gamma;) -v- (unit G))</code>:
 
 <pre>
-       (5) Consider the composite transformation ((M &gamma;) -v- (unit G)). This assigns to C1 the morphism M(&gamma;*) &#8728; unit[G(C1)].
+       (5) ((M &gamma;) -v- (unit G)) assigns to C1 the morphism M(&gamma;*) &#8728; unit[G(C1)].
 </pre>
 
-Next:
+Next, consider the composite transformation <code>((unit MG') -v- &gamma;)</code>:
 
 <pre>
-       (6) Consider the composite transformation ((unit MG') -v- &gamma;). This assigns to C1 the morphism unit[MG'(C1)] &#8728; &gamma;*.
+       (6) ((unit MG') -v- &gamma;) assigns to C1 the morphism unit[MG'(C1)] &#8728; &gamma;*.
 </pre>
 
 So for every element C1 of <b>C</b>:
@@ -466,8 +466,8 @@ Collecting the results, our monad laws turn out in this format to be:
 
 
 
-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.