On 3 Aug 2010, at 12:03, Paul Levy wrote:
On 3 Aug 2010, at 07:39, Richard Garner wrote:
Dear Paul,
Thanks for your perspicuous message.
And thanks for your more perspicuous reply! Your argument apparently applies to both coproduct and tensor of strong monads, and also to a free strong monad on a strong endofunctor. Each of these can be characterized both by a universal property and by a left adjoint to a forgetful functor from an algebra category. Nice.
Your general definition of tensor product really cuts to the heart of the matter, and agrees with the cases where I knew how to take tensors previously. Has it been written down somewhere? It seems very natural.
The universal property is alluded to in the TCS paper "Combining effects: sum and tensor" by Hyland, Plotkin and Power: page 4, paragraph beginning "There is also relevant unpublished work by Paul Levy". I gave up on it (i.e. the universal property) thinking it was too weak. Now you've shown me it wasn't.
I should also have said that the universal property - though not the notion of "commuting S,T-algebra" in the form I stated it - did appear in the paper Combining algebraic effects with continuations, by Hyland, me, Plotkin and Power. Sorry for forgetting this, it's been a while. Also, the proof of Theorem 4 (and also that of Prop. 3) is similar to the one you provided, although the result is somewhat different. Paul -- Paul Blain Levy School of Computer Science, University of Birmingham +44 (0)121 414 4792 http://www.cs.bham.ac.uk/~pbl [For admin and other information see: http://www.mta.ca/~cat-dist/ ]