From 9905c7069d7b4d2f8b9ffbeccaa12d6c64382a8a Mon Sep 17 00:00:00 2001 From: Jim Pryor Date: Tue, 2 Nov 2010 11:52:45 -0400 Subject: [PATCH] cat theory tweaks Signed-off-by: Jim Pryor --- advanced_topics/monads_in_category_theory.mdwn | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) 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)) -- 2.11.0