A cartesian multicategory is a multicategory-like structure which is related to categories with finite products in the same way that ordinary multicategories are related to monoidal categories.
A cartesian multicategory is a symmetric multicategory equipped with:
duplication or diagonal or contraction operations
deletion or projection or weakening operations
which satisfy certain evident axioms.
A cartesian multicategory can equivalently be defined as a generalized multicategory relative to the monad on Cat (or more precisely Prof) whose algebras are categories with (strict) finite products.
A cartesian multicategory can also be defined as a category with specified finite products whose set of objects under the “product” operation is a free monoid on specified generators.
When there is exactly one such generator, this recovers the definition of a Lawvere theory; thus a cartesian multicategory may be considered a “colored” or “many-object” Lawvere theory. Note, though, that the morphisms of cartesian multicategories are more restrictive than morphisms of finite-product categories; they are required to take generators to generators.
A cartesian multicategory, like an ordinary multicategory, is representable if for any finite list $(c_1,\dots,c_n)$ of objects there exists an object “$c_1 \times \cdots \times c_n$” and a morphism $c_1,\dots,c_n \to c_1 \times \cdots \times c_n$ which is universal, in that the following induced functions are all bijections:
Just as representable (symmetric) multicategories are equivalent to (symmetric) monoidal categories, representable cartesian multicategories are equivalent to cartesian monoidal categories.
More abstractly, representable cartesian multicategories are the algebras for a colax-idempotent 2-monad on the 2-category of cartesian multicategories, whose algebras are categories with finite products.
Small cartesian multicategories may be considered presentations of “many-sorted finite-product theories”. On the spectrum between syntax and semantics, they sit in between a fully syntactic presentation (such as a type theory) and a fully incarnated semantic one (the free category with finite products generated by a model of some theory).
Cartesian multicategories are also a natural place to talk about the semantics of type theory. Every type theory (with contraction and weakening, and without dependent types) gives rise to a cartesian multicategory whose objects are its types and whose multimorphisms are its terms. This is in contrast to the usual construction of an ordinary category from a type theory, in which we have to take the objects to be contexts in order to recapture all the terms. This usual category of contexts can be recaptured as the free category-with-finite-products generated by this cartesian multicategory of types. Similarly, we can talk about models of such a type theory in any cartesian multicategory.
Last revised on September 4, 2020 at 09:31:00. See the history of this page for a list of all contributions to it.