X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=advanced_topics%2Fmonads_in_category_theory.mdwn;h=24670796b21e1fc3cd230352e0049772bf17a2b3;hp=1d7ede7167c1c9fdeed424ea8925725c30308232;hb=ac47fea0dc57a0f496d14dba80383206397a35f9;hpb=d6f9a31a5eadc6270f0c97d63d9e97f11b5081f5 diff --git a/advanced_topics/monads_in_category_theory.mdwn b/advanced_topics/monads_in_category_theory.mdwn index 1d7ede71..24670796 100644 --- a/advanced_topics/monads_in_category_theory.mdwn +++ b/advanced_topics/monads_in_category_theory.mdwn @@ -393,87 +393,83 @@ Finally, we substitute ((join G') -v- (M γ) -v- φ) for - (ρ <=< γ) is a transformation from G to MR', so: - (ρ <=< γ) <=< φ becomes: (join R') (M (ρ <=< γ)) φ - which is: (join R') (M ((join R') (M ρ) γ)) φ - substituting in (ii), and helping ourselves to associativity on the rhs, we get: + (ρ <=< γ) is a transformation from G to MR', so + (ρ <=< γ) <=< φ becomes: ((join R') (M (ρ <=< γ)) φ) + which is: ((join R') (M ((join R') (M ρ) γ)) φ) - ((join R') (M ((join R') (M ρ) γ)) φ) = ((join R') (M ρ) (join G') (M γ) φ) + similarly, ρ <=< (γ <=< φ) is: + ((join R') (M ρ) ((join G') (M γ) φ)) + + substituting these into (ii), and helping ourselves to associativity on the rhs, we get: + ((join R') (M ((join R') (M ρ) γ)) φ) = ((join R') (M ρ) (join G') (M γ) φ) - which by the distributivity of functors over composition, and helping ourselves to associativity on the lhs, yields: - - ((join R') (M join R') (MM ρ) (M γ) φ) = ((join R') (M ρ) (join G') (M γ) φ) + which by the distributivity of functors over composition, and helping ourselves to associativity on the lhs, yields: + ((join R') (M join R') (MM ρ) (M γ) φ) = ((join R') (M ρ) (join G') (M γ) φ) - which by lemma 1, with ρ a transformation from G' to MR', yields: - - ((join R') (M join R') (MM ρ) (M γ) φ) = ((join R') (join MR') (MM ρ) (M γ) φ) - - which will be true for all ρ,γ,φ just in case: + which by lemma 1, with ρ a transformation from G' to MR', yields: + ((join R') (M join R') (MM ρ) (M γ) φ) = ((join R') (join MR') (MM ρ) (M γ) φ) - ((join R') (M join R')) = ((join R') (join MR')), for any R'. + which will be true for all ρ,γ,φ only when: + ((join R') (M join R')) = ((join R') (join MR')), for any R'. - which will in turn be true just in case: - - (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') <=< γ = γ when γ is a natural transformation from some FG' to MG' - (iii.1) (unit F') <=< φ = φ ==> - (unit F') is a transformation from F' to MF', so: - (unit F') <=< φ becomes: (join F') (M unit F') φ - which is: (join F') (M unit F') φ - substituting in (iii.1), we get: - ((join F') (M unit F') φ) = φ - - which will be true for all φ just in case: + (unit G') is a transformation from G' to MG', so: + (unit G') <=< γ becomes: ((join G') (M unit G') γ) - ((join F') (M unit F')) = the identity transformation, for any F' + substituting in (iii.1), we get: + ((join G') (M unit G') γ) = γ - which will in turn be true just in case: + which will be true for all γ 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) γ = γ <=< (unit G) + (iii.2) γ = γ <=< (unit G) when γ is a natural transformation from G to some MR'G - (iii.2) φ = φ <=< (unit F) ==> - φ is a transformation from F to MF', so: - unit <=< φ becomes: (join F') (M φ) unit - substituting in (iii.2), we get: - φ = ((join F') (M φ) (unit F)) - -------------- - which by lemma (2), yields: - ------------ - φ = ((join F') ((unit MF') φ) - - which will be true for all φ just in case: - - ((join F') (unit MF')) = the identity transformation, for any F' - - which will in turn be true just in case: - + unit <=< γ becomes: ((join R'G) (M γ) unit) + + substituting in (iii.2), we get: + γ = ((join R'G) (M γ) (unit G)) + + which by lemma 2, yields: + γ = ((join R'G) ((unit MR'G) γ) + + which will be true for all γ 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 Collecting the results, our monad laws turn out in this format to be: - - when φ a transformation from F to MF', γ a transformation from F' to MG', ρ a transformation from G' to MR' all in T: +
+	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') ((join G') (M γ) φ) etc also in T
+	    (i') ((join G') (M γ) φ) 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