author Jim Pryor Tue, 2 Nov 2010 15:44:36 +0000 (11:44 -0400) committer Jim Pryor Tue, 2 Nov 2010 15:44:36 +0000 (11:44 -0400)
Signed-off-by: Jim Pryor <profjim@jimpryor.net>

index 0c60f2e..1d7ede7 100644 (file)
@@ -379,14 +379,19 @@ So our **(lemma 2)** is:
Finally, we substitute <code>((join G') -v- (M &gamma;) -v- &phi;)</code> for <code>&gamma; &lt;=&lt; &phi;</code> in the monad laws. For simplicity, I'll omit the "-v-".

<pre>
-       for all &phi;,&gamma;,&rho; in T, where &phi; is a transformation from F to MF', &gamma; is a transformation from G to MG', R is a transformation from R to MR', and F'=G and G'=R:
+       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) &gamma; <=< &phi; etc are also in T
+            (i) &gamma; <=< &phi; etc are also in T
==>
-       (i') ((join G') (M &gamma;) &phi;) etc are also in T
+           (i') ((join G') (M &gamma;) &phi;) etc are also in T

-       (ii) (&rho; <=< &gamma;) <=< &phi;  =  &rho; <=< (&gamma; <=< &phi;)
+
+           (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;
@@ -394,13 +399,13 @@ Finally, we substitute <code>((join G') -v- (M &gamma;) -v- &phi;)</code> for <c
substituting in (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 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; just in case:
@@ -409,9 +414,12 @@ Finally, we substitute <code>((join G') -v- (M &gamma;) -v- &phi;)</code> for <c

which will in turn be true just in case:

-       (ii') (join (M join)) = (join (join M))
+          (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:
@@ -429,6 +437,10 @@ Finally, we substitute <code>((join G') -v- (M &gamma;) -v- &phi;)</code> for <c
(iii.1') (join (M unit) = the identity transformation

+
+
+        (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: