Jason (jcreed) wrote,

So I had this hazy idea that one might be able to think about logics with funny contexts in terms of a funny generalization of multicategories. Multicategories are like categories where each arrow has for its domain a list of objects instead of just one object. The concept of list is, to me anyhow, an archetypal example of a monad, so it's sensible to try to replace it with an arbitrary monad, to replace the idea of list-of-hypotheses with crazy-data-structure-of-hypotheses. The place I got stuck trying to work this out was in the middle of one of understanding some other definitions in another one of Baez's papers, so I sent him an email asking about it; it turns out from the response I got this morning that Tom Leinster has basically already written an entire book answering my question! How courteous of him. On page 109 of this thing, the definition of T-multicategories (as monads in a certain 2-category of spans) is trumpeted as "[...]the most important definition in this book" and apparently goes all the way back to 1971. Surely someone has to have worked out the meaning of this thing in logic by now, then. I'm beginning more to wonder why I haven't already heard of all this stuff.

The really sad part is that the condition on the monad T that gives the structure of the context is that it needs to preserve pullbacks (and so too the natural transformations η and μ in the monad need all their naturality squares to be pullbacks) and the "free commutative monoid" monad doesn't have this property. So naïvely setting up, say, bunched logic in terms of a monad that takes the free structure with two commutative monoids, one of them with contraction and weakening, looks like a total no-go. On the other hand, something about symmetry is obviously workable, since operads and multicatories equipped with a symmetry "on the outside" are totally well-understood. It's troubling that one can't independently sneak symmetries into things by just adding (non-strongly regular) equational laws.
Tags: math, work

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 1 comment