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 588d1a3..90f77cb 100644 (file)
--- a/advanced_topics/monads_in_category_theory.mdwn
+++ b/advanced_topics/monads_in_category_theory.mdwn
@@ -393,70 +393,64 @@ Finally, we substitute <code>((join G') -v- (M &gamma;) -v- &phi;)</code> for <c
 
            (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;)
+                    (&rho; <=< &gamma;) is a transformation from G to MR', so
+                        (&rho; <=< &gamma;) <=< &phi; becomes: ((join R') (M (&rho; <=< &gamma;)) &phi;)
                                                        which is: ((join R') (M ((join R') (M &rho;) &gamma;)) &phi;)
 
-                       similarly, &rho; <=< (&gamma; <=< &phi;) is:
+                        similarly, &rho; <=< (&gamma; <=< &phi;) is:
                                                        ((join R') (M &rho;) ((join G') (M &gamma;) &phi;))
 
-                       substituting these into (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;)
+                        substituting these into (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 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 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; only when:
-               ((join R') (M join R')) = ((join R') (join MR')), for any R'.
+                        which will be true for all &rho;,&gamma;,&phi; only when:
+                ((join R') (M join R')) = ((join R') (join MR')), for any R'.
 
-                       which will in turn be true when:
-      (ii') (join (M join)) = (join (join M))
+                        which will in turn be true when:
+       (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:
-                               (unit F') <=< &phi; becomes: (join F') (M unit F') &phi;
-                                                  which is: (join F') (M unit F') &phi;
-                               substituting in (iii.1), we get:
-                       ((join F') (M unit F') &phi;) = &phi;
+                        (unit G') is a transformation from G' to MG', so:
+                        (unit G') <=< &gamma; becomes: ((join G') (M unit G') &gamma;)
+                                                   which is: ((join G') (M unit G') &gamma;)
 
-                       which will be true for all &phi; just in case:
+                        substituting in (iii.1), we get:
+                        ((join G') (M unit G') &gamma;) = &gamma;
 
-                ((join F') (M unit F')) = the identity transformation, for any F'
-
-                       which will in turn be true just in case:
+                        which will be true for all &gamma; just in case:
+                ((join G') (M unit G')) = the identity transformation, for any G'
 
+                        which will in turn be true just in case:
        (iii.1') (join (M unit) = the identity transformation
 
 
 
 
-        (iii.2)                     &gamma;  =  &gamma; <=< (unit G)
+        (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:
-                               unit <=< &phi; becomes: (join F') (M &phi;) unit
-                               substituting in (iii.2), we get:
-                       &phi; = ((join F') (M &phi;) (unit F))
-                                                  --------------
-                               which by lemma (2), yields:
-                            ------------
-                       &phi; = ((join F') ((unit MF') &phi;)
-
-                               which will be true for all &phi; just in case:
-
-               ((join F') (unit MF')) = the identity transformation, for any F'
-
-                               which will in turn be true just in case:
-
+                        unit <=< &gamma; becomes: (join R'G) (M &gamma;) unit
+                       
+                        substituting in (iii.2), we get:
+                        &gamma; = ((join R'G) (M &gamma;) (unit G))
+               
+                        which by lemma 2, yields:
+                        &gamma; = ((join R'G) ((unit MR'G) &gamma;)
+
+                         which will be true for all &gamma; just in case:
+                ((join R'G) (unit MR'G)) = the identity transformation, for any R'G
+
+                        which will in turn be true just in case:
        (iii.2') (join (unit M)) = the identity transformation
 </pre>
 
@@ -464,15 +458,15 @@ Finally, we substitute <code>((join G') -v- (M &gamma;) -v- &phi;)</code> for <c
 Collecting the results, our monad laws turn out in this format to be:
 
 </pre>
-       when &phi; a transformation from F to MF', &gamma; a transformation from F' to MG', &rho; a transformation from G' to MR' all in T:
+       when &phi; a transformation from F to MF', &gamma; a transformation from F' to MG', &rho; a transformation from G' to MR' are all in T:
 
-       (i') ((join G') (M &gamma;) &phi;) etc also in T
+           (i') ((join G') (M &gamma;) &phi;) etc also in T
 
-       (ii') (join (M join)) = (join (join M))
+          (ii') (join (M join)) = (join (join M))
 
        (iii.1') (join (M unit)) = the identity transformation
 
-       (iii.2')(join (unit M)) = the identity transformation
+       (iii.2') (join (unit M)) = the identity transformation
 </pre>