From: Jim Pryor Date: Tue, 2 Nov 2010 15:44:36 +0000 (-0400) Subject: cat theory tweaks X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=d6f9a31a5eadc6270f0c97d63d9e97f11b5081f5 cat theory tweaks Signed-off-by: Jim Pryor --- diff --git a/advanced_topics/monads_in_category_theory.mdwn b/advanced_topics/monads_in_category_theory.mdwn index 0c60f2e5..1d7ede71 100644 --- a/advanced_topics/monads_in_category_theory.mdwn +++ b/advanced_topics/monads_in_category_theory.mdwn @@ -379,14 +379,19 @@ So our **(lemma 2)** is: Finally, we substitute ((join G') -v- (M γ) -v- φ) for γ <=< φ in the monad laws. For simplicity, I'll omit the "-v-". 
-	for all φ,γ,ρ in T, where φ is a transformation from F to MF', γ is a transformation from G to MG', R is a transformation from R to MR', and F'=G and G'=R:
+	For all ρ, γ, φ in T,
+	where φ is a transformation from F to MF',
+	γ is a transformation from G to MG',
+	ρ is a transformation from R to MR',
+	and F'=G and G'=R:
 
-	(i) γ <=< φ etc are also in T
+	     (i) γ <=< φ etc are also in T
 	==>
-	(i') ((join G') (M γ) φ) etc are also in T
+	    (i') ((join G') (M γ) φ) etc are also in T
 
 
-	(ii) (ρ <=< γ) <=< φ  =  ρ <=< (γ <=< φ)
+
+	    (ii) (ρ <=< γ) <=< φ  =  ρ <=< (γ <=< φ)
 	==>
 		 (ρ <=< γ) is a transformation from G to MR', so:
 			(ρ <=< γ) <=< φ becomes: (join R') (M (ρ <=< γ)) φ
@@ -394,13 +399,13 @@ Finally, we substitute ((join G') -v- (M γ) -v- φ) for ((join G') -v- (M γ) -v- φ) for 
 			(unit F') is a transformation from F' to MF', so:
@@ -429,6 +437,10 @@ Finally, we substitute ((join G') -v- (M γ) -v- φ) for 
 			φ is a transformation from F to MF', so: