cat theory tweaks

Signed-off-by: Jim Pryor <profjim@jimpryor.net>

diff --git a/advanced_topics/monads_in_category_theory.mdwn b/advanced_topics/monads_in_category_theory.mdwn
index f05747f..0c60f2e 100644 (file)
--- a/advanced_topics/monads_in_category_theory.mdwn
+++ b/advanced_topics/monads_in_category_theory.mdwn
@@ -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 `<=<`.
 
 <!--
 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>.
 
 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)]`.
 
 
 *      `(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>
 
        (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>
 
 <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>:
 </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>
 
        (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>
 
 <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>
 
 </pre>
 

-Next:
+Next, consider the composite transformation <code>((unit MG') -v- &gamma;)</code>:

 
 <pre>
 
 <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>:
 </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.
 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.