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=588d1a30f237dcad0f82b0a26d875af84b9459da;hp=0c60f2e54c3580470f198435bdcef47a579127dc;hb=c0a6070f7c11da38419b5e5da90afeddc6520b95;hpb=06c94f923bb5f17d440d24dadca280a57fb8f6f5
diff --git a/advanced_topics/monads_in_category_theory.mdwn b/advanced_topics/monads_in_category_theory.mdwn
index 0c60f2e5..588d1a30 100644
--- a/advanced_topics/monads_in_category_theory.mdwn
+++ b/advanced_topics/monads_in_category_theory.mdwn
@@ -379,39 +379,46 @@ 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 (ρ <=< γ)) φ
- 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 ρ) γ)) φ)
+
+ similarly, ρ <=< (γ <=< φ) is:
+ ((join R') (M ρ) ((join G') (M γ) φ))
- ((join R') (M ((join R') (M ρ) γ)) φ) = ((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:
+ which will be true for all ρ,γ,φ only when:
+ ((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 when:
+ (ii') (join (M join)) = (join (join M))
- which will in turn be true just in case:
-
- (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:
@@ -429,6 +436,10 @@ Finally, we substitute ((join G') -v- (M γ) -v- φ) for
φ is a transformation from F to MF', so: