author Jim Pryor Tue, 2 Nov 2010 16:12:04 +0000 (12:12 -0400) committer Jim Pryor Tue, 2 Nov 2010 16:12:04 +0000 (12:12 -0400)
Signed-off-by: Jim Pryor <profjim@jimpryor.net>

index 90f77cb..2467079 100644 (file)
@@ -422,7 +422,6 @@ Finally, we substitute <code>((join G') -v- (M &gamma;) -v- &phi;)</code> for <c
==>
(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;)

substituting in (iii.1), we get:
((join G') (M unit G') &gamma;) = &gamma;
@@ -439,7 +438,7 @@ Finally, we substitute <code>((join G') -v- (M &gamma;) -v- &phi;)</code> for <c
(iii.2) &gamma;  =  &gamma; <=< (unit G)
when &gamma; is a natural transformation from G to some MR'G
==>
-                        unit <=< &gamma; becomes: (join R'G) (M &gamma;) unit
+                        unit <=< &gamma; becomes: ((join R'G) (M &gamma;) unit)

substituting in (iii.2), we get:
&gamma; = ((join R'G) (M &gamma;) (unit G))
@@ -457,8 +456,12 @@ 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' are all in T:
+<pre>
+       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') ((join G') (M &gamma;) &phi;) etc also in T