From: Jim Pryor <profjim@jimpryor.net>
Date: Tue, 2 Nov 2010 15:39:13 +0000 (-0400)
Subject: cat theory tweaks
X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=06c94f923bb5f17d440d24dadca280a57fb8f6f5;ds=sidebyside

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 f05747f6..0c60f2e5 100644
--- 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 `<=<`.
 
 <!--
@@ -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.