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=768b8542a6e22019ce98a8f09fda446bd537145c;hp=fe12655bac9e24310213d1616279771202565bd0;hb=636bebd66c03835ae35ec9b38b82485c4ae6460b;hpb=2f14eb20bd2428f346f8d5c8caa35b67eb043096
diff --git a/advanced_topics/monads_in_category_theory.mdwn b/advanced_topics/monads_in_category_theory.mdwn
index fe12655b..768b8542 100644
--- a/advanced_topics/monads_in_category_theory.mdwn
+++ b/advanced_topics/monads_in_category_theory.mdwn
@@ -213,25 +213,25 @@ Now we can specify the "monad laws" governing a monad as follows:
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
+ (i) γ `<=<` φ is also in T
- (ii) (ρ <=< γ) <=< φ = ρ <=< (γ <=< φ)
+ (ii) (ρ `<=<` γ) `<=<` φ = ρ `<=<` (γ `<=<` φ)
- (iii.1) unit <=< φ = φ (here φ has to be a natural transformation to M(1C))
+ (iii.1) unit `<=<` φ = φ (here φ has to be a natural transformation to M(1C))
- (iii.2) φ = φ <=< unit (here φ has to be a natural transformation from 1C)
+ (iii.2) φ = φ `<=<` unit (here φ has to be a natural transformation from 1C)
If φ is a natural transformation from `F` to `M(1C)` and γ is (φ G'), that is, a natural transformation from `FG` to `MG`, then we can extend (iii.1) as follows:
γ = (φ G')
- = ((unit <=< φ) G')
+ = ((unit `<=<` φ) G')
= ((join -v- (M unit) -v- φ) G')
= (join G') -v- ((M unit) G') -v- (φ G')
= (join G') -v- (M (unit G')) -v- γ
??
- = (unit G') <=< γ
+ = (unit G') `<=<` γ
where as we said γ is a natural transformation from some `FG'` to `MG'`.
@@ -240,12 +240,12 @@ Similarly, if φ is a natural transformation from `1C` to `MF'`,
γ = (φ G)
- = ((φ <=< unit) G)
+ = ((φ `<=<` unit) G)
= (((join F') -v- (M φ) -v- unit) G)
= ((join F'G) -v- ((M φ) G) -v- (unit G))
= ((join F'G) -v- (M (φ G)) -v- (unit G))
??
- = γ <=< (unit G)
+ = γ `<=<` (unit G)
where as we said γ is a natural transformation from `G` to some `MF'G`.
@@ -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)).