nLab cartesian multicategory

Idea

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.

Definition

Explicit

A cartesian multicategory is a symmetric multicategory equipped with:

• duplication or diagonal or contraction operations

  $$hom(c_0,\dots,c_{k-1},c_k,c_k,c_{k+1},\dots,c_{n-1} \;;\; d) \to hom(c_0,\dots,c_{k-1},c_k,c_{k+1},\dots,c_{n-1} \;;\; d)$$

• deletion or projection or weakening operations

  $$hom(c_0,\dots,c_{k-1},c_{k+1},\dots,c_{n-1} \;;\; d) \to hom(c_0,\dots,c_{k-1},c_k,c_{k+1},\dots,c_{n-1} \;;\; d)$$

which satisfy certain evident axioms.

As a generalized multicategory

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.

As a free category with 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.

Alternative presentation

The composition structure of a cartesian multicategory can also be equivalently presented in the style usually used for abstract clones. The symmetry, contraction and weakening are derivable rather than required. In this style, a cartesian multicategory is given by a collection of objects, and for every sequence $c_1\dots c_{n+1}$ of objects, a collection of multimorphisms $hom(c_1\dots c_{n}\;;\;c_{n+1})$, and

• for every sequence $c_{1}\dots c_{n}$ and $i\leq n$, a projection map

  $$\pi_{i} \in hom(c_{1} \dots c_{n} \;;\; c_{i})$$

• for sequences $c_1\dots c_m$, $d_1\dots d_{n}$ and object $e$, a composition map

  $$\circ : hom(d_1\dots d_{n} \;;\; e)\times \prod_{i=1}^{n} hom(c_1\dots c_m \;;\; d_i)\to hom(c_1\dots c_m,e)$$

all such that

• identity laws: $f\circ (\pi_i)_i = f$ and $\pi_i \circ (f_0\dots f_{n-1})=f_i$;

• associativity law: $f\circ (g_1\circ (h_1\dots h_{n})\dots g_{m}\circ (h_1\dots h_{n})) = f \circ (g_1\dots g_{m}) \circ (h_1\dots h_{n})$.

Representability

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:

$$hom(d_1,\dots,d_k, c_1 \times \cdots \times c_n , e_1,\dots,e_m \;;\; f) \to hom(d_1,\dots,d_k, c_1,\dots,c_n, e_1,\dots,e_m \;;\; f)$$

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.

Syntax, semantics, and type theory

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.

Related pages

• multicategory
• symmetric multicategory
• generalized multicategory
• Lawvere theory
• A cartesian multicategory with one object is equivalent to an abstract clone. More generally, cartesian multicategories are equivalent to multisorted abstract clones.
• sequential multicategory

References

Cartesian multicategories were introduced under the name Gentzen multicategories in §10 of:

• Joachim Lambek, Multicategories revisited, Categories in Computer Science and Logic 92 (1989): 217-240.

They are called finite product multicategories in the following reference. The author proves that cartesian operads are monadic over symmetric operads, which are monadic over operads, which are monadic over $\mathbb{N}$-indexed sets.

• Miles Gould, Coherence for categorified operadic theories, PhD thesis, University of Glasgow, 2008.

• Claudio Pisani, Sequential multicategories, (arXiv:1402.0253)

• Nathanael Arkor and Dylan McDermott, Abstract Clones for Abstract Syntax, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2021. (arXiv)