From f11472452da56243652ffeed1f56b418f6b6c1dd Mon Sep 17 00:00:00 2001 From: Jim Pryor Date: Tue, 2 Nov 2010 09:13:26 -0400 Subject: [PATCH] cat theory tweaks Signed-off-by: Jim Pryor --- advanced_topics/monads_in_category_theory.mdwn | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) diff --git a/advanced_topics/monads_in_category_theory.mdwn b/advanced_topics/monads_in_category_theory.mdwn index a6165e9d..966fc95c 100644 --- a/advanced_topics/monads_in_category_theory.mdwn +++ b/advanced_topics/monads_in_category_theory.mdwn @@ -202,20 +202,25 @@ 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 its 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'` which = `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 `F` is a functor to `MF'` and `G` is a functor 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
+
 	   (ii) (ρ <=< γ) <=< φ  =  ρ <=< (γ <=< φ)
+
 	(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)
+
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: @@ -229,7 +234,7 @@ If φ is a natural transformation from `F` to `M(1C)` and where as we said γ is a natural transformation from some `FG'` to `MG'`. -Similarly, if φ is a natural transformation from `1C` to `MF'`, and γ is `(φ G)`, that is, a natural transformation from `G` to `MF'G`, then we can extend (iii.2) as follows: +Similarly, if φ is a natural transformation from `1C` to `MF'`, and γ is (φ G), that is, a natural transformation from `G` to `MF'G`, then we can extend (iii.2) as follows: γ = (φ G) = ((φ <=< unit) G) @@ -239,7 +244,7 @@ Similarly, if φ is a natural transformation from `1C` to `MF'`, and γ ?? = γ <=< (unit G) -where as we said γ is a natural transformation from `G` to some `MF'G`. +where as we said γ is a natural transformation from `G` to some `MF'G`. -- 2.11.0