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=c0d4bf7f8cc08712dcd6f3824aadf0f2ae59c6f9;hp=fe12655bac9e24310213d1616279771202565bd0;hb=86c716d4c3d50b20cd1fbf426e139c07629641aa;hpb=2f14eb20bd2428f346f8d5c8caa35b67eb043096
diff --git a/advanced_topics/monads_in_category_theory.mdwn b/advanced_topics/monads_in_category_theory.mdwn
index fe12655b..c0d4bf7f 100644
--- a/advanced_topics/monads_in_category_theory.mdwn
+++ b/advanced_topics/monads_in_category_theory.mdwn
@@ -202,15 +202,15 @@ Let φ and γ be members of `T`, that is they
Since composition is associative I don't specify the order of composition on the rhs.
-In other words, `<=<` is a binary operator that takes us from two members φ and γ of `T` to a composite natural transformation. (In functional programming, at least, this is called the "Kleisli composition operator". Sometimes it's written φ >=> γ where that's the same as γ <=< φ.)
+In other words, `<=<` is a binary operator that takes us from two members φ and γ of `T` to a composite natural transformation. (In functional programming, at least, this is called the "Kleisli composition operator". Sometimes it's written φ >=> γ where that's the same as γ <=< φ.)
-φ is a transformation from `F` to `MF'`, where the latter = `MG`; (M γ) is a transformation from `MG` to `MMG'`; and `(join G')` is a transformation from `MMG'` to `MG'`. So the composite γ <=< φ will be a transformation from `F` to `MG'`, and so also eligible to be a member of `T`.
+φ is a transformation from `F` to `MF'`, where the latter = `MG`; (M γ) is a transformation from `MG` to `MMG'`; and `(join G')` is a transformation from `MMG'` to `MG'`. So the composite γ <=< φ will be a transformation from `F` to `MG'`, and so also eligible to be a member of `T`.
Now we can specify the "monad laws" governing a monad as follows:
(T, <=<, unit) constitute a monoid
-That's it. Well, there may be a wrinkle here. I don't know whether the definition of a monoid requires the operation to be defined for every pair in its set. In the present case, γ <=< φ isn't fully defined on `T`, but only when φ is a transformation to some `MF'` and γ is a transformation from `F'`. But wherever `<=<` is defined, the monoid laws are satisfied:
+That's it. Well, there may be a wrinkle here. I don't know whether the definition of a monoid requires the operation to be defined for every pair in its set. In the present case, γ <=< φ isn't fully defined on `T`, but only when φ is a transformation to some `MF'` and γ is a transformation from `F'`. But wherever `<=<` is defined, the monoid laws are satisfied:
(i) γ <=< φ is also in T
@@ -288,7 +288,7 @@ Next, consider the composite transformation ((join MG') -v- (MM γ))<
Composing them:
- (2) ((join MG') -v- (MM γ)) assigns to `C1` the morphism join[MG'(C1)] ∘ MM(γ*).
+ (2) ((join MG') -v- (MM γ)) assigns to `C1` the morphism join[MG'(C1)] ∘ MM(γ*).
Next, consider the composite transformation ((M γ) -v- (join G)).
@@ -347,7 +347,7 @@ 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-".
+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: