Categorifying the observation that monoids are generalized elements of multicategories, we show that unbiased pseudomonoids, such as unbiased monoidal categories, are “pseudo-elements” of 2-multicategories.
(I’m going to comment here and on the original post)
Great post Evan!
I think that multicategories are very natural from a programming perspective, because we have functions which take multiple arguments and return one thing, and these are different from functions that take a single tuple argument.
I think we could push this closer to programming practice by doing an equivalent (but not isomorphic) presentation of multicategories, where instead of having a category of morphisms for every objects (X_1,\ldots,X_n;Y), we fix a set of strings \Sigma, and have a category of morphisms for every finite subset X_{-} \colon L \subset \Sigma^*, function L \to \mathrm{Ob}, and then Y \in \mathrm{Ob}. We consider L \subset \Sigma^* because we want “paths of symbols”. I.e., a.b, or wheel.force. This would be a T-multicategory for the polynomial monad T = \sum_{L \subset \Sigma^*} y^L., where the functor T \triangleleft T \to T concatenates the labels. That is, if \mathtt{a} \mapsto \{\mathtt{x}, \mathtt{y}\}, \mathtt{b} \mapsto \{\mathtt{q}, \mathtt{p}\}, then we end up with the label set \{\mathtt{a}.\mathtt{x}, \mathtt{a}.\mathtt{y}, \mathtt{b}.\mathtt{q}, \mathtt{b}.\mathtt{p}\}.
I’m just sketching out the idea here; the details would have to include throwing in isomorphisms whenever we have a bijection L \cong L'. But the point is, then we would have some notion of 2-multicategory, where the pseudo-elements were categories equipped with a “record formation” operation for every L \subset \Sigma^\ast. I think that we have to use something like this in order to have an algebraic presentation of symmetric monoidal categories that is actually convenient to program in.
Thanks Owen!
Yes, if I understand you correctly, there is another presentation of symmetric multicategories where instead of having lists of objects with an action by permutations, you have finite sets typed by the objects along with an action by FinBij. Leinster calls these “fat symmetric multicategories” and gives a proper definition in Appendix A of his book.
It would be awesome to have a generic approach to multicategories of various flavors (bare, symmetric, cartesian) in Catlab. We can’t do that with GATs, or at least not our flavor of GATs, because the theory of multicategories doesn’t seem to have a finite presentation.
Oh excellent, I’m glad that Leinster covers these. I think that even though these aren’t GATs, we can reuse some of the GAT machinery in Gatlab (i.e. scopes/names, and interfaces via modules) to work with this sort of thing.