cat theory tweaks

[lambda.git] / advanced_topics / monads_in_category_theory.mdwn

diff --git a/advanced_topics/monads_in_category_theory.mdwn b/advanced_topics/monads_in_category_theory.mdwn
index 1d7ede7..402a5e7 100644 (file)
--- a/advanced_topics/monads_in_category_theory.mdwn
+++ b/advanced_topics/monads_in_category_theory.mdwn
@@ -393,28 +393,28 @@ 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;
-                                                       which is: (join R') (M ((join R') (M &rho;) &gamma;)) &phi;
-                       substituting in (ii), and helping ourselves to associativity on the rhs, we get:
+                   (&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;)
 
-            ((join R') (M ((join R') (M &rho;) &gamma;)) &phi;) = ((join R') (M &rho;) (join G') (M &gamma;) &phi;)
+                       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;)
     
                        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;)
+              ((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;)
+              ((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:
-
-             ((join R') (M join R')) = ((join R') (join MR')), for any R'.
+               ((join R') (M join R')) = ((join R') (join MR')), for any R'.
 
                        which will in turn be true just in case:
 
-          (ii') (join (M join)) = (join (join M))
+      (ii') (join (M join)) = (join (join M))