tweak cat theory

Signed-off-by: Jim Pryor <profjim@jimpryor.net>

diff --git a/advanced_topics/monads_in_category_theory.mdwn b/advanced_topics/monads_in_category_theory.mdwn
index 6ebcd8d..173e986 100644 (file)
--- a/advanced_topics/monads_in_category_theory.mdwn
+++ b/advanced_topics/monads_in_category_theory.mdwn
@@ -11,7 +11,7 @@ functional programming uses of these notions in enough detail to be sure that
 none of the pieces here is misguided. In particular, it wasn't completely
 obvious how to map the polymorphism on the programming theory side into the
 category theory. And I'm bothered by the fact that our `<=<` operation is only
 none of the pieces here is misguided. In particular, it wasn't completely
 obvious how to map the polymorphism on the programming theory side into the
 category theory. And I'm bothered by the fact that our `<=<` operation is only

-partly defined on our domain of natural transformations. But these do seem to
+partly defined on our domain of natural transformations. But this does seem to

 me to be the reasonable way to put the pieces together. We very much welcome
 feedback from anyone who understands these issues better, and will make
 corrections.
 me to be the reasonable way to put the pieces together. We very much welcome
 feedback from anyone who understands these issues better, and will make
 corrections.


@@ -176,7 +176,7 @@ That's it. (Well, perhaps we're cheating a bit, because `q <=< p` isn't fully de
 
        (i) q <=< p is also in T
        (ii) (r <=< q) <=< p  =  r <=< (q <=< p)
 
        (i) q <=< p is also in T
        (ii) (r <=< q) <=< p  =  r <=< (q <=< p)

-       (iii.1) unit <=< p  =  p  (here p has to be a natural transformation to M(1C))
+       (iii.1) unit <=< p  =  p                 (here p has to be a natural transformation to M(1C))

        (iii.2)                p  =  p <=< unit  (here p has to be a natural transformation from 1C)
 
 If `p` is a natural transformation from `P` to `M(1C)` and `q` is `(p Q')`, that is, a natural transformation from `PQ` to `MQ`, then we can extend (iii.1) as follows:
        (iii.2)                p  =  p <=< unit  (here p has to be a natural transformation from 1C)
 
 If `p` is a natural transformation from `P` to `M(1C)` and `q` is `(p Q')`, that is, a natural transformation from `PQ` to `MQ`, then we can extend (iii.1) as follows:


@@ -186,6 +186,7 @@ If `p` is a natural transformation from `P` to `M(1C)` and `q` is `(p Q')`, that
          = ((join -v- (M unit) -v- p) Q')
          = (join Q') -v- ((M unit) Q') -v- (p Q')
          = (join Q') -v- (M (unit Q')) -v- q
          = ((join -v- (M unit) -v- p) Q')
          = (join Q') -v- ((M unit) Q') -v- (p Q')
          = (join Q') -v- (M (unit Q')) -v- q

+         ??

          = (unit Q') <=< q
 
 where as we said `q` is a natural transformation from some `PQ'` to `MQ'`.
          = (unit Q') <=< q
 
 where as we said `q` is a natural transformation from some `PQ'` to `MQ'`.


@@ -194,9 +195,10 @@ Similarly, if `p` is a natural transformation from `1C` to `MP'`, and `q` is `(p
 
        q = (p Q)
          = ((p <=< unit) Q)
 
        q = (p Q)
          = ((p <=< unit) Q)

-         = (((join P') (M p) unit) Q)
-         = ((join P'Q) ((M p) Q) (unit Q))
-         = ?
+         = (((join P') -v- (M p) -v- unit) Q)
+         = ((join P'Q) -v- ((M p) Q) -v- (unit Q))
+         = ((join P'Q) -v- (M (p Q)) -v- (unit Q))
+         ??

          = q <=< (unit Q)
 
 where as we said `q` is a natural transformation from `Q` to some `MP'Q`. 
          = q <=< (unit Q)
 
 where as we said `q` is a natural transformation from `Q` to some `MP'Q`. 


@@ -206,7 +208,7 @@ where as we said `q` is a natural transformation from `Q` to some `MP'Q`.
 
 The standard category-theory presentation of the monad laws
 -----------------------------------------------------------
 
 The standard category-theory presentation of the monad laws
 -----------------------------------------------------------

-In category theory, the monad laws are usually stated in terms of unit and join instead of unit and <=<.
+In category theory, the monad laws are usually stated in terms of `unit` and `join` instead of `unit` and `<=<`.

 
 (*
        P2. every element c1 of a category C has an identity morphism id[c1] such that for every morphism f:c1->c2 in C: id[c2] o f = f = f o id[c1].
 
 (*
        P2. every element c1 of a category C has an identity morphism id[c1] such that for every morphism f:c1->c2 in C: id[c2] o f = f = f o id[c1].