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=33f9bf3894a72046eaeb169d8c2aacd45b155211;hp=deb5bace5b8656474b48d69a80d985c9bf5c493d;hb=d752bea8fab7d8a83e1704ca99d37dd5dfcc52f3;hpb=4bc7f125d288c543b0d22f9f8e69775dc9460317
diff --git a/advanced_topics/monads_in_category_theory.mdwn b/advanced_topics/monads_in_category_theory.mdwn
index deb5bace..33f9bf38 100644
--- a/advanced_topics/monads_in_category_theory.mdwn
+++ b/advanced_topics/monads_in_category_theory.mdwn
@@ -233,7 +233,8 @@ If φ is a natural transformation from `F` to `M(1C)` and
= (((join 1C) G') -v- ((M unit) G') -v- (φ G'))
= ((join (1C G')) -v- (M (unit G')) -v- γ)
= ((join G') -v- (M (unit G')) -v- γ)
- since (unit G') is a natural transformation to MG', this satisfies the definition for <=<:
+ since (unit G') is a natural transformation to MG',
+ this satisfies the definition for <=<:
= (unit G') <=< γ
@@ -247,12 +248,28 @@ Similarly, if ρ is a natural transformation from `1C` to `MR'`,
= (((join R') -v- (M ρ) -v- unit) G)
= (((join R') G) -v- ((M ρ) G) -v- (unit G))
= ((join (R'G)) -v- (M (ρ G)) -v- (unit G))
- since γ = (ρ G) is a natural transformation to MR'G, this satisfies the definition for <=<:
+ since γ = (ρ G) is a natural transformation to MR'G,
+ this satisfies the definition <=<:
= γ <=< (unit G)
where as we said γ is a natural transformation from `G` to some `MR'G`.
+Summarizing then, the monad laws can be expressed as:
+
+
+ For all γ, φ in T for which ρ <=< γ and γ <=< φ are defined:
+
+ (i) γ <=< φ is also in T
+
+ (ii) (ρ <=< γ) <=< φ = ρ <=< (γ <=< φ)
+
+ (iii.1) (unit G') <=< γ = γ
+ when γ is a natural transformation from some FG' to MG'
+
+ (iii.2) γ = γ <=< (unit G)
+ when γ is a natural transformation from G to some MR'G
+