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 deb5bac..0db16cb 100644 (file)
--- a/advanced_topics/monads_in_category_theory.mdwn
+++ b/advanced_topics/monads_in_category_theory.mdwn
@@ -233,7 +233,8 @@ If <code>&phi;</code> is a natural transformation from `F` to `M(1C)` and <code>
          = (((join 1C) G') -v- ((M unit) G') -v- (&phi; G'))
          = ((join (1C G')) -v- (M (unit G')) -v- &gamma;)
          = ((join G') -v- (M (unit G')) -v- &gamma;)
-         since (unit G') is a natural transformation to MG', this satisfies the definition for <=<:
+         since (unit G') is a natural transformation to MG',
+         this satisfies the definition for &lt;=&lt;:
          = (unit G') <=< &gamma;
 </pre>
 
@@ -247,12 +248,28 @@ Similarly, if <code>&rho;</code> is a natural transformation from `1C` to `MR'`,
          = (((join R') -v- (M &rho;) -v- unit) G)
          = (((join R') G) -v- ((M &rho;) G) -v- (unit G))
          = ((join (R'G)) -v- (M (&rho; G)) -v- (unit G))
-         since &gamma; = (&rho; G) is a natural transformation to MR'G, this satisfies the definition for <=<:
+         since &gamma; = (&rho; G) is a natural transformation to MR'G,
+         this satisfies the definition &lt;=&lt;:
          = &gamma; <=< (unit G)
 </pre>
 
 where as we said <code>&gamma;</code> is a natural transformation from `G` to some `MR'G`.
 
+Summarizing then, the monad laws can be expressed as:
+
+<pre>
+       For all &gamma;, &phi; in T for which &rho; <=< &gamma; and &gamma; <=< &phi; are defined:
+
+           (i) &gamma; <=< &phi; is also in T
+
+          (ii) (&rho; <=< &gamma;) <=< &phi;  =  &rho; <=< (&gamma; <=< &phi;)
+
+       (iii.1) (unit G') <=< &gamma;  =  &gamma;
+               when &gamma; is a natural transformation from some FG' to MG'
+
+       (iii.2) &gamma;  =  &gamma; <=< (unit G)
+               when &gamma; is a natural transformation from G to some MR'G
+</pre>