From a40cca61ecb584096b4e304508c4a2d0d477555e Mon Sep 17 00:00:00 2001 From: Jim Pryor Date: Tue, 2 Nov 2010 12:07:37 -0400 Subject: [PATCH] cat theory tweaks Signed-off-by: Jim Pryor --- advanced_topics/monads_in_category_theory.mdwn | 82 ++++++++++++-------------- 1 file changed, 38 insertions(+), 44 deletions(-) diff --git a/advanced_topics/monads_in_category_theory.mdwn b/advanced_topics/monads_in_category_theory.mdwn index 588d1a30..90f77cbe 100644 --- a/advanced_topics/monads_in_category_theory.mdwn +++ b/advanced_topics/monads_in_category_theory.mdwn @@ -393,70 +393,64 @@ Finally, we substitute ((join G') -v- (M γ) -v- φ) for - (ρ <=< γ) is a transformation from G to MR', so - (ρ <=< γ) <=< φ becomes: ((join R') (M (ρ <=< γ)) φ) + (ρ <=< γ) is a transformation from G to MR', so + (ρ <=< γ) <=< φ becomes: ((join R') (M (ρ <=< γ)) φ) which is: ((join R') (M ((join R') (M ρ) γ)) φ) - similarly, ρ <=< (γ <=< φ) is: + similarly, ρ <=< (γ <=< φ) is: ((join R') (M ρ) ((join G') (M γ) φ)) - substituting these into (ii), and helping ourselves to associativity on the rhs, we get: - ((join R') (M ((join R') (M ρ) γ)) φ) = ((join R') (M ρ) (join G') (M γ) φ) + substituting these into (ii), and helping ourselves to associativity on the rhs, we get: + ((join R') (M ((join R') (M ρ) γ)) φ) = ((join R') (M ρ) (join G') (M γ) φ) - which by the distributivity of functors over composition, and helping ourselves to associativity on the lhs, yields: - ((join R') (M join R') (MM ρ) (M γ) φ) = ((join R') (M ρ) (join G') (M γ) φ) + which by the distributivity of functors over composition, and helping ourselves to associativity on the lhs, yields: + ((join R') (M join R') (MM ρ) (M γ) φ) = ((join R') (M ρ) (join G') (M γ) φ) - which by lemma 1, with ρ a transformation from G' to MR', yields: - ((join R') (M join R') (MM ρ) (M γ) φ) = ((join R') (join MR') (MM ρ) (M γ) φ) + which by lemma 1, with ρ a transformation from G' to MR', yields: + ((join R') (M join R') (MM ρ) (M γ) φ) = ((join R') (join MR') (MM ρ) (M γ) φ) - which will be true for all ρ,γ,φ only when: - ((join R') (M join R')) = ((join R') (join MR')), for any R'. + which will be true for all ρ,γ,φ only when: + ((join R') (M join R')) = ((join R') (join MR')), for any R'. - which will in turn be true when: - (ii') (join (M join)) = (join (join M)) + which will in turn be true when: + (ii') (join (M join)) = (join (join M)) (iii.1) (unit G') <=< γ = γ when γ is a natural transformation from some FG' to MG' - (iii.1) (unit F') <=< φ = φ ==> - (unit F') is a transformation from F' to MF', so: - (unit F') <=< φ becomes: (join F') (M unit F') φ - which is: (join F') (M unit F') φ - substituting in (iii.1), we get: - ((join F') (M unit F') φ) = φ + (unit G') is a transformation from G' to MG', so: + (unit G') <=< γ becomes: ((join G') (M unit G') γ) + which is: ((join G') (M unit G') γ) - which will be true for all φ just in case: + substituting in (iii.1), we get: + ((join G') (M unit G') γ) = γ - ((join F') (M unit F')) = the identity transformation, for any F' - - which will in turn be true just in case: + which will be true for all γ just in case: + ((join G') (M unit G')) = the identity transformation, for any G' + which will in turn be true just in case: (iii.1') (join (M unit) = the identity transformation - (iii.2) γ = γ <=< (unit G) + (iii.2) γ = γ <=< (unit G) when γ is a natural transformation from G to some MR'G - (iii.2) φ = φ <=< (unit F) ==> - φ is a transformation from F to MF', so: - unit <=< φ becomes: (join F') (M φ) unit - substituting in (iii.2), we get: - φ = ((join F') (M φ) (unit F)) - -------------- - which by lemma (2), yields: - ------------ - φ = ((join F') ((unit MF') φ) - - which will be true for all φ just in case: - - ((join F') (unit MF')) = the identity transformation, for any F' - - which will in turn be true just in case: - + unit <=< γ becomes: (join R'G) (M γ) unit + + substituting in (iii.2), we get: + γ = ((join R'G) (M γ) (unit G)) + + which by lemma 2, yields: + γ = ((join R'G) ((unit MR'G) γ) + + which will be true for all γ just in case: + ((join R'G) (unit MR'G)) = the identity transformation, for any R'G + + which will in turn be true just in case: (iii.2') (join (unit M)) = the identity transformation @@ -464,15 +458,15 @@ Finally, we substitute ((join G') -v- (M γ) -v- φ) for - when φ a transformation from F to MF', γ a transformation from F' to MG', ρ a transformation from G' to MR' all in T: + when φ a transformation from F to MF', γ a transformation from F' to MG', ρ a transformation from G' to MR' are all in T: - (i') ((join G') (M γ) φ) etc also in T + (i') ((join G') (M γ) φ) etc also in T - (ii') (join (M join)) = (join (join M)) + (ii') (join (M join)) = (join (join M)) (iii.1') (join (M unit)) = the identity transformation - (iii.2')(join (unit M)) = the identity transformation + (iii.2') (join (unit M)) = the identity transformation -- 2.11.0