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

index 588d1a3..90f77cb 100644 (file)
@@ -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>