From: Jim Pryor Date: Tue, 2 Nov 2010 15:52:45 +0000 (-0400) Subject: cat theory tweaks X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=9905c7069d7b4d2f8b9ffbeccaa12d6c64382a8a 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 1d7ede71..402a5e77 100644 --- a/advanced_topics/monads_in_category_theory.mdwn +++ b/advanced_topics/monads_in_category_theory.mdwn @@ -393,28 +393,28 @@ 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 γ) φ) + ((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 γ) φ) + ((join R') (M join R') (MM ρ) (M γ) φ) = ((join R') (join MR') (MM ρ) (M γ) φ) which will be true for all ρ,γ,φ just in case: - - ((join R') (M join R')) = ((join R') (join MR')), for any R'. + ((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)) + (ii') (join (M join)) = (join (join M))