In this article, we explore cartesian monoidal categories as a doctrine on Cat, by analyzing the structure of free cartesian categories.
It is convenient to discuss the case of categories with arbitrary small products (or arbitrary small coproducts) first, because there we get some very pleasant adjunctions to work with. Then, we may cut down to finite products and derive some possibly unexpected bonuses involving finite limits.
We start by constructing the free category with small products generated by a set $S$. This by definition is a category with small products, $Prod(S)$, equipped with a function $i: S \to Ob(Prod(S))$ with the following universal property: given a category $C$ with small products and a function $f: S \to Ob(C)$, there exists up to (unique) isomorphism a unique product-preserving functor $\Pi: Prod(S) \to C$ such that $f = Ob(\Pi) \circ i$.
The slice category $Set/S$ is small-cocomplete; therefore $(Set/S)^{op}$ has small products. There is an evident function $i: S \to Ob((Set/S)^{op})$ which takes $s \in S$ to $s: 1 \to S$. This can also be regarded as a Yoneda embedding under the equivalence $Set/S \simeq Set^S$.
Each object $n: N \to S$ of $(Set/S)^{op}$ can be regarded as a formal product $\prod_{s \in S} x_{s}^{n_s}$ where $S$ indexes a set of variables $x_s$ and $n_s = n^{-1}(s)$ is the (cardinality of the) fiber over $S$. Therefore the following theorem comes as no surprise.
$(Set/S)^{op}$ together with $i: S \to (Set/S)^{op}$ is the free category with small products generated by $S$.
Let $C$ be a category with small products. Given $f: S \to Ob(C)$, the functor $\Pi: (Set/S)^{op} \to C$ is defined on the object-level: $n: N \to S$ is sent to $\prod_{s \in S} f(s)^{n_s}$ in $C$. In addition, a morphism from $m: M \to S$ to $n: N \to S$ in $(Set/S)^{op}$ is a function $\phi: N \to M$ that satisfies $m \circ \phi = n$; this in turn consists of a collection of functions $\phi_s: n_s \to m_s$ indexed by elements $s \in S$, and each such function induces a morphism
in $C$, uniquely specified by declaring the $i^{th}$ component of this morphism for $i \in n_s$ to be given by
Given a morphism $\phi$ of $(Set/S)^{op}$, define $\Pi(\phi)$ by
The functor $\Pi$ is the unique product-preserving functor $(Set/S)^{op} \to C$ (up to isomorphism) that extends $f: S \to Ob(C)$.
Given categories with products $C$ and $D$, let $\mathbf{Prod}(C, D)$ denote the category of product-preserving functors $F: C \to D$ and natural transformations between them. By the preceding theorem, there is an equivalence
where the right side consists of functors $S \to C$ (where $S$ is regarded as a discrete category) and natural transformations between them.
The category $\mathbf{Prod}((Set/S)^{op}, Set)$ is isomorphic to $Set/S$.
Because $\mathbf{Prod}((Set/S)^{op}, Set) \simeq Set^S \simeq Set/S$.
Let $C$ be a locally small category with products. There is a Yoneda embedding
As we just saw, the Yoneda embedding $y: Set/S \to \mathbf{Prod}((Set/S)^{op}, Set)$ is an equivalence. We may arrange that the reverse equivalence $\mathbf{Prod}((Set/S)^{op}, Set) \to Set/S$ is right adjoint to $y$, and so we denote it as $y^*$.
If $C$ is a locally small category with small products and $f: S \to C$ is a functor, the coproduct-preserving functor $\Pi^{op}: Set/S \to C^{op}$ has a right adjoint given by the composite
Let $g: X \to S$ be an object of $Set/S$ and $c$ an object of $C$. We have the following natural bijections between sets of morphisms:
where we get to the third line by the Yoneda lemma. This proves the theorem.
Under the hypotheses of the previous theorem, the product-preserving functor $\Pi: (Set/S)^{op} \to C$ is a right adjoint. In particular, it preserves all limits, not just products.
It will be convenient to consider first the coproduct-cocompletion; then the product-completion is obtained by dualizing.
Let $C$ be a small category. We may construct the free category with coproducts generated by $C$ directly as follows:
The objects of $Coprod(C)$ are those of $Set/C_0$, where $C_0$ is the set of objects.
A morphism (say from $f: X \to C_0$ to $g: Y \to C_0$) is given by a function $\phi: X \to Y$ together with an $X$-indexed collection of morphisms of $C$ of the form $\Phi_x: f(x) \to g(\phi(x))$.
The data of a morphism may be exhibited as a 2-cell of the form
Coproducts of objects in $Coprod(C)$ are computed just as they are in $Set/C_0$. Each $f: X \to C_0$ is then a formal coproduct $\sum_x f(x)$, and a morphism $(\phi, \Phi): \sum_{x \in X} f(x) \to \sum_{y \in Y} g(y)$ is uniquely determined by its restrictions along the coprojections $i_x: f(x) \to \sum_x f(x)$, which in turn are given by composites
where $y = \phi(x)$. The proof of the universal property of $Coprod(C)$ as coproduct cocompletion is then obvious.
Another light on this construction comes from seeing the free coproduct-cocompletion $Coprod(C)$ as sitting inside the free cocompletion $Set^{C^{op}}$. First, we have a Yoneda mapping
This induces a coproduct-preserving functor $Set/C_0 \to Set^{C^{op}}$, which takes an object $g: Y \to C_0$ to the presheaf
By the preceding theorem, this functor has a right adjoint. The right adjoint is simply described: it is the evident underlying functor
taking a presheaf $F: C^{op} \to Set$ to the $C_0$-indexed set where the fiber over $c \in C_0$ is $F(c)$.
As is well-known, this underlying functor $Set^{C^{op}} \to Set/C_0$ is monadic; the monad $M_C$ takes an object $g: Y \to C_0$ to the object whose fiber over $c$ is the set
In other words, the left adjoint to the underlying functor is the coproduct-preserving functor that takes $g: Y \to C_0$ to
as described above.
Notice that $M_C(g)$ is given by the top horizontal composite
where the square is a pullback.
The free coproduct-cocompletion of $C$ is the Kleisli category of the monad $M_C: Set/C_0 \to Set/C_0$.
Let $f: X \to C_0$ and $g: Y \to C_0$ be two objects of $Kl(M_C)$. A morphism from $f$ to $g$ in $Kl(M_C)$ is a morphism from $f$ to $M_C(g)$ in $Set/C_0$, in other words a map $h: X \to P$ making the following diagram commute:
Since $P$ is the pullback, the map $h$ is given by maps $\phi: X \to Y$, $\Phi: X \to C_1$ with $\Phi(x): f(x) \to g(\phi(x))$ for each $x \in X$. But this is how a morphism from $f$ to $g$ was described in the explicit construction of $Coprod(C)$.
We calculate the free coproduct completion of the interval category $\mathbf{2} = (0 \to 1)$, and record some properties of this category.
According to theorem 3, this is the Kleisli category of the monad on $Set/\{0, 1\}$ corresponding to the monadic functor $Set^{\mathbf{2}^{op}} \to Set/\{0, 1\}$. This monad takes a pair of sets $(X_1, X_0)$ to $(X_1, X_0 + X_1)$; the algebra structure of the free algebra $(X_1, X_0 + X_1)$ is the structure of presheaf over $\mathbf{2}$ given by the inclusion $X_1 \hookrightarrow X_0 + X_1$.
Thus the free coproduct completion of $\mathbf{2}$ is equivalent to the category $Subset$ who objects are pairs of sets $(A, X)$ where $A$ is a subset of $X$; morphisms $(A, X) \to (B, Y)$ are functions $f: X \to Y$ which carry $A$ into $B$.
This category has many pleasant properties, largely summarized by the fact that it is a Grothendieck quasitopos. Indeed, it can be described as the category of $\neg \neg$-separated presheaves on $\mathbf{2}$ (so that it is a reflective subcategory of $Set^{\mathbf{2}^{op}}$). The reflection takes an object $f: X \to Y$ to the pair $(Im(f), Y)$.
In particular, $Subset$ is complete and cocomplete and cartesian closed. Limits are formed as they are in $Set^{\mathbf{2}^{op}}$ (that is, objectwise). As are exponentials, since $Subset$ is actually an exponential ideal in $Set^{\mathbf{2}^{op}}$. Naturally, coproducts are formed as they are in the presheaf category since $Subset$ is the coproduct completion; coequalizers are constructed by forming them in the presheaf category and then reflecting back into $Subset$.
Categories enriched in $Subset$ are also called M-categories.
The free product-completion of $C$ is obtained by dualization:
Here $M = M_{C^{op}}$ is the monad on $Set/C_0$ whose algebras are functors $C \to Set$. This functor category is the category of models of a simple multi-sorted algebraic theory, where the set of sorts is $C_0$ and each morphism $f: c \to d$ is regarded as an unary operation. According to the entry algebraic theory, the corresponding Lawvere theory is just $Kl(M)^{op}$, in other words the product-completion of $C$. Indeed, the category of models of $Kl(M)^{op}$ is
by the universal property of $Prod(C)$.
There is no foundational difficulty in forming the free small coproduct-cocompletion of any locally small category $C$ (any more than forming the free cocompletion with respect to small limits). An object of $Coprod(C)$ is a set $X$ together with a function $f: X \to C_0$. A morphism from $f: X \to C_0$ to $g: Y \to C_0$ consists of a function $\phi: X \to Y$ together with an $X$-indexed collection of morphisms $\Phi_x: f(x) \to g(\phi(x))$. The hom-sets are clearly small.
To be continued
There are a number of ways of explaining the same material from a more categorical point of view. Whatever the explanation is, the point is to describe the free category with finite products generated from a multigraph $F$ over $S$. We denote this free category with products as $Term(S, F)$.
As before, the objects of $Term(S, F)$ are product types: elements of $S^\ast$. Morphisms from a type $T: [m] \to S$ to a type $T': [n] \to S$ are, in the language of the preceding section, $n$-tuples of normal terms $(t_1, \ldots, t_n)$ where each $t_i$ has arity $T \to T'(i)$. Composition is effected by term substitution. The cartesian product structure is essentially given by concatenating (juxtaposing) lists of sorts and terms.
It is hopefully more or less clear how all of this works in the term syntax approach. Despite this, we believe that the bureaucracy of handling variables in the term syntax is something of a hack; from one point of view (closely related to string diagrams), some of it is actually unnecessary.
For example, the input strings play the role of variables declared in the context, but the difference is that they do not need “variable names” – they only need to be labeled by an appropriate sort, for type-checking purposes. This trick effectively eliminates the need for rules of $\alpha$-conversion. As we will see, one can also effect a neat division of labor between the business of variable declarations and the business of “pure substitutions”; moreover, this division clarifies the precise entry point of the particular doctrine we are working in (the doctrine of finite product categories).
To begin, recall the following abstract definition:
Let $M$ be a cartesian monad acting on a finitely complete category $C$. An $M$-span in $C$ from $c$ to $d$ is a span of the form
$M$-spans are composed by consideration of a pullback
where $m: M M \to M$ is the multiplication on the monad $M$. Under this composition, the $M$-spans are 1-cells of a bicategory $M$-$Span$.
In the case where $M$ is the free monoid monad acting on $Set$, an $M$-span from a set $S$ to $S$ is the same as a multigraph over $S$. A monad on $S$ in the bicategory $M$-$Span$ is a multicategory over $S$. We are especially interested in the free multicategory generated from a multigraph over $S$.
The free multicategory construction has other names and descriptions. We could also call it the free nonpermutative $S$-sorted operad generated by a set of $S$-typed function symbols. The apex of its underlying span, together with its map to $S$, can also be referred to as the initial algebra for the polynomial endofunctor $P$ on $Set/S$ which takes an $S$-indexed set $X_s$ to
($f \in F$). However it is named, the underlying multigraph of the free multicategory generated by a multigraph $F$ can be described as
where $Tree(F)$ is the set of $F$-labeled planar trees. This means that
Nodes of a planar tree are labeled by elements $f: T \to s$ of $F$;
Edges of that planar tree are labeled by sorts $s$, such that the list of labels of incoming edges at a node $f: T \to s$ is the word $T$, and the outgoing edge is labeled $s$.
The list of labels of “leaves” of an $F$-labeled tree $t$ (edges that are not outgoing edges of any node) gives an element $in(t) \in S^\ast$, and the label of the “root” edge gives an element $out(t) \in S$. Notice that $F$-labeled trees have obvious string diagram representations.
Next, any multicategory generates a (strict monoidal) category. In the present instance, we denote this category as $Pro(S, F)$ (we write “Pro” by analogy with “prop” – whereas props are used for the doctrine of symmetric monoidal categories, pros are used for monoidal categories). The objects of $Pro(S, F)$ are elements of $S^\ast$. The morphisms of $Pro(S, F)$ could be described as ”$F$-labeled forests”. Formally, the underlying span of $Pro(S, F)$ is
The monoidal product on forests is simply juxtaposition. The composition of forests is the obvious one, plugging in roots of one forest for leaves of another.
The construction $Pro(S, F)$ formalizes what we meant earlier by “pure substitutions of terms”, and lives in the doctrine of (strict) monoidal categories. To switch over to the doctrine of categories with finite cartesian products, we apply a simple trick. Let $Pro(S, F) \circ Prod(S)$ be the composite of the two spans
Then, in the first place, $Pro(S, F) \circ Prod(S)$ carries a canonical category structure. The reason is that, viewing $Prod(S)$ and $Pro(S, F)$ as monads in the bicategory of spans, there is a canonical distributive law
(here $Pro(S, F)$ can be replaced by any pro over $S$). The idea is that the distributive law $\theta$ maps an element of $Prod(S) \circ Pro(S, F)$, which is a pair of arrows
with $f$ an arrow of $Pro(S, F)$ and $d$ an arrow of $Prod(S)$, to a pair of arrows in $Pro(S, F) \circ Prod(S)$ whose precise form is dictated by a naturality requirement in $d$. For example, if $d = \delta_T': T' \to T' \otimes T'$, then
Using this distributive law, the composite of the monads $Prod(S)$ and $Pro(S, F)$ is another monad in the bicategory of spans, and therefore a category with set of objects $S^\ast$.
The same trick works for other doctrines over the doctrine of monoidal categories. For example, if $Perm(S)$ is the free symmetric (strict) monoidal category generated by $S$, regarded as a span from $S^\ast$ to $S^\ast$, then there is a distributive law $Perm(S) \circ Pro(S, F) \to Pro(S, F) \circ Perm(S)$. Similarly with “symmetric monoidal” replaced with “braided monoidal”.
$Term(S, F) \coloneqq Pro(S, F) \circ Prod(S)$, regarded as a cartesian category with product structure inherited from $Prod(S)$, meaning that
is a product-preserving functor, where $u$ is the unit of the monad $Pro(S, F)$.
More explicitly, the tensor product $\bigotimes$ on $Term(S, F)$ is a cartesian product provided that there are natural transformations $\delta: id \to \otimes \Delta$, $\varepsilon: id \to e !$ which endow each object with a cocommutative comonoid structure. But the naturality follows from the definition of the distributive law, and the cocommutative comonoid axioms already hold in $Prod(S)$.
Note that this abstract description of $Term(S, F)$ is identical to that given by the syntax of normal terms. The “bureaucracy of variables” is here organized into two departments, $Prod(S)$ and $Pro(S, F)$, each having its own individual categorical structure, which interact via the distributive law. (This is the “division of labor” we were talking about, where each arrow of $Term(S, F)$ is factorized into a generalized diagonal map followed by an $F$-labeled forest.)
Another name for $Term(S, F)$ is “term algebra”, and yet another name for it is “the free $S$-sorted Lawvere theory generated by a set of $S$-sorted operation symbols $F$”.
$Term(S, F)$ is the free category with products generated by the multigraph $F$ over $S$.
$Tree(S, F)$ is the free multicategory generated by the multigraph $F$ over $S$, and $Pro(S, F)$ is the free monoidal category generated by the multicategory $Tree(S, F)$. Therefore $Pro(S, F)$ is the free monoidal category generated by the multigraph $F$. It remains to show that the monoidal inclusion
is universal among monoidal functors $X: Pro(S, F) \to C$ to cartesian monoidal categories $C$.
There is of course a product-preserving functor $Prod(S) \to C$ compatible with the restriction $S^\ast \hookrightarrow Pro(S, F) \stackrel{X}{\to} C$. At the level of spans, this gives a composable pair of span morphisms
which we then compose with the span morphism $m: C_1 \circ C_1 \to C_1$ given by composition in $C$:
This gives a morphism between underlying spans, $Term(S, F) \to C$. This is functorial (i.e., is a morphism of monads in $Span$) because both $Prod(S) \to C$ and $Pro(S, F) \to C$ are functorial, and also because the compositional equalities enforced by the distributive law $\theta$ are preserved: they are taken to equalities expressed by naturality of diagonal maps and projection maps in $C$. The functor $Term(S, F) \to C$ is product-preserving, because $Prod(S) \to C$ is product-preserving. The uniqueness of the product-preserving extension $Term(S, F) \to C$ is clear since the subcategories $Prod(S)$ and $Pro(S, F)$ together generate $Term(S, F)$.