Multicategory of commutative monoids

[laMudri]

I think the (symmetric) multicategory of commutative monoids would be a good benchmark for any definition of (symmetric) multicategories. In this multicategory, objects are commutative monoids and morphisms are multilinear maps, i.e, maps f : A₁ × … × Aₙ → B such that f(a₁, …, x + y, …, aₙ) = f(a₁, …, x, …, aₙ) + f(a₁, …, y, …, aₙ) at each position in the domain. I like this benchmark for two reasons:

• It is the simplest example I can think of that isn't based on type theory/logic. It may turn out that modules over commutative semirings are easier to mechanise (with commutative monoids being exactly ℕ-modules), in which case I would accept that way of passing the benchmark.
• It is a prototype for a practical use of multicategories for (linear) algebra. Multilinear maps give a way to give a universal property to tensor products. It would be a big win if we could reason abstractly with such tensor products, because the construction of those tensor products is very technical, and is the kind of thing best avoided in mechanisations.

I have previously had difficulty defining this multicategory based on the definition in this library. We may consider whether a direct definition of symmetric multicategories is simpler than a definition of general multicategories. Indeed, a direct definition of Cartesian multicategories is much easier, and I nearly have the techniques in my upcoming thesis to define symmetric multicategories in a similar way.

I believe that if composition is stated in the simultaneous style (compare: simultaneous substitution), then we need to build in finiteness at some point. In the single style, we might get away without it because single compositions are inherently finitary. The current definition uses the simultaneous style, which is maybe a desideratum; in type theory, simultaneous substitution is generally the preferred foundation.