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

index 402a5e7..588d1a3 100644 (file)
@@ -404,16 +404,15 @@ Finally, we substitute <code>((join G') -v- (M &gamma;) -v- &phi;)</code> for <c
((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:
+                       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 just in case:
-
+                       which will in turn be true when:
(ii') (join (M join)) = (join (join M))