X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=advanced_topics%2Fmonads_in_category_theory.mdwn;fp=advanced_topics%2Fmonads_in_category_theory.mdwn;h=402a5e778d16520463b1d149ffe54661d55ea02c;hp=1d7ede7167c1c9fdeed424ea8925725c30308232;hb=9905c7069d7b4d2f8b9ffbeccaa12d6c64382a8a;hpb=d6f9a31a5eadc6270f0c97d63d9e97f11b5081f5
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))