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 0c60f2e..1d7ede7 100644 (file)
--- a/advanced_topics/monads_in_category_theory.mdwn
+++ b/advanced_topics/monads_in_category_theory.mdwn
@@ -379,14 +379,19 @@ So our **(lemma 2)** is:
 Finally, we substitute <code>((join G') -v- (M &gamma;) -v- &phi;)</code> for <code>&gamma; &lt;=&lt; &phi;</code> in the monad laws. For simplicity, I'll omit the "-v-".
 
 <pre>
-       for all &phi;,&gamma;,&rho; in T, where &phi; is a transformation from F to MF', &gamma; is a transformation from G to MG', R is a transformation from R to MR', and F'=G and G'=R:
+       For all &rho;, &gamma;, &phi; in T,
+       where &phi; is a transformation from F to MF',
+       &gamma; is a transformation from G to MG',
+       &rho; is a transformation from R to MR',
+       and F'=G and G'=R:
 
-       (i) &gamma; <=< &phi; etc are also in T
+            (i) &gamma; <=< &phi; etc are also in T
        ==>
-       (i') ((join G') (M &gamma;) &phi;) etc are also in T
+           (i') ((join G') (M &gamma;) &phi;) etc are also in T
 
 
-       (ii) (&rho; <=< &gamma;) <=< &phi;  =  &rho; <=< (&gamma; <=< &phi;)
+
+           (ii) (&rho; <=< &gamma;) <=< &phi;  =  &rho; <=< (&gamma; <=< &phi;)
        ==>
                 (&rho; <=< &gamma;) is a transformation from G to MR', so:
                        (&rho; <=< &gamma;) <=< &phi; becomes: (join R') (M (&rho; <=< &gamma;)) &phi;
@@ -394,13 +399,13 @@ Finally, we substitute <code>((join G') -v- (M &gamma;) -v- &phi;)</code> for <c
                        substituting in (ii), and helping ourselves to associativity on the rhs, we get:
 
             ((join R') (M ((join R') (M &rho;) &gamma;)) &phi;) = ((join R') (M &rho;) (join G') (M &gamma;) &phi;)
-                     ---------------------
+    
                        which by the distributivity of functors over composition, and helping ourselves to associativity on the lhs, yields:
-                    ------------------------
+   
             ((join R') (M join R') (MM &rho;) (M &gamma;) &phi;) = ((join R') (M &rho;) (join G') (M &gamma;) &phi;)
-                                                             ---------------
+  
                        which by lemma 1, with &rho; a transformation from G' to MR', yields:
-                                                             -----------------
+ 
             ((join R') (M join R') (MM &rho;) (M &gamma;) &phi;) = ((join R') (join MR') (MM &rho;) (M &gamma;) &phi;)
 
                        which will be true for all &rho;,&gamma;,&phi; just in case:
@@ -409,9 +414,12 @@ Finally, we substitute <code>((join G') -v- (M &gamma;) -v- &phi;)</code> for <c
 
                        which will in turn be true just in case:
 
-       (ii') (join (M join)) = (join (join M))
+          (ii') (join (M join)) = (join (join M))
+
 
 
+        (iii.1) (unit G') <=< &gamma;  =  &gamma;
+                when &gamma; is a natural transformation from some FG' to MG'
        (iii.1) (unit F') <=< &phi;  =  &phi;
        ==>
                        (unit F') is a transformation from F' to MF', so:
@@ -429,6 +437,10 @@ Finally, we substitute <code>((join G') -v- (M &gamma;) -v- &phi;)</code> for <c
        (iii.1') (join (M unit) = the identity transformation
 
 
+
+
+        (iii.2)                     &gamma;  =  &gamma; <=< (unit G)
+                when &gamma; is a natural transformation from G to some MR'G
        (iii.2) &phi;  =  &phi; <=< (unit F)
        ==>
                        &phi; is a transformation from F to MF', so: