From: Jim Pryor Date: Tue, 2 Nov 2010 13:33:00 +0000 (-0400) Subject: cat theory tweaks X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=86c716d4c3d50b20cd1fbf426e139c07629641aa cat theory tweaks Signed-off-by: Jim Pryor --- diff --git a/advanced_topics/monads_in_category_theory.mdwn b/advanced_topics/monads_in_category_theory.mdwn index 768b8542..c0d4bf7f 100644 --- a/advanced_topics/monads_in_category_theory.mdwn +++ b/advanced_topics/monads_in_category_theory.mdwn @@ -202,36 +202,36 @@ 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
+	    (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`. @@ -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: