nLab
free cartesian category

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.

Free product-completions of sets

We start by constructing the free category with small products generated by a set $S$. This by definition is a category with small products, $\mathrm{Prod}(S)$, equipped with a function $i:S\to \mathrm{Ob}(\mathrm{Prod}(S))$ with the following universal property: given a category $C$ with small products and a function $f:S\to \mathrm{Ob}(C)$, there exists up to (unique) isomorphism a unique product-preserving functor $\Pi :\mathrm{Prod}(S)\to C$ such that $f=\mathrm{Ob}(\Pi )\circ i$.

The slice category $\mathrm{Set}/S$ is small-cocomplete; therefore $(\mathrm{Set}/S{)}^{\mathrm{op}}$ has small products. There is an evident function $i:S\to \mathrm{Ob}((\mathrm{Set}/S{)}^{\mathrm{op}})$ which takes $s\in S$ to $s:1\to S$. This can also be regarded as a Yoneda embedding under the equivalence $\mathrm{Set}/S\simeq {\mathrm{Set}}^S$.

Each object $n:N\to S$ of $(\mathrm{Set}/S{)}^{\mathrm{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.

Theorem

$(\mathrm{Set}/S{)}^{\mathrm{op}}$ together with $i:S\to (\mathrm{Set}/S{)}^{\mathrm{op}}$ is the free category with small products generated by $S$.

Proof

Let $C$ be a category with small products. Given $f:S\to \mathrm{Ob}(C)$, the functor $\Pi :(\mathrm{Set}/S{)}^{\mathrm{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 $(\mathrm{Set}/S{)}^{\mathrm{op}}$ is a function $\varphi :N\to M$ that satisfies $m\circ \varphi =n$; this in turn consists of a collection of functions ${\varphi }_s:n_s\to m_s$ indexed by elements $s\in S$, and each such function induces a morphism

$$f(s{)}^{{\varphi }_s}:f(s{)}^{m_s}\to f(s{)}^{n_s}$$f(s)^{\phi_s}: f(s)^{m_s} \to f(s)^{n_s}

in $C$, uniquely specified by declaring the $i^{\mathrm{th}}$ component of this morphism for $i\in n_s$ to be given by

$$f(s{)}^{m_s}\stackrel{{\mathrm{proj}}_{{\varphi }_s(i)}}{\to }f(s)$$f(s)^{m_s} \stackrel{proj_{\phi_s(i)}}{\to} f(s)

Given a morphism $\varphi$ of $(\mathrm{Set}/S{)}^{\mathrm{op}}$, define $\Pi (\varphi )$ by

$$\Pi (\varphi )=⟨f(s{)}^{{\varphi }_s}{⟩}_{s\in S}:\prod _{s\in S}f(s{)}^{m_s}\to \prod _{s\in S}f(s{)}^{n_s}.$$\Pi(\phi) = \langle f(s)^{\phi_s} \rangle_{s \in S}: \prod_{s \in S} f(s)^{m_s} \to \prod_{s \in S} f(s)^{n_s}.

The functor $\Pi$ is the unique product-preserving functor $(\mathrm{Set}/S{)}^{\mathrm{op}}\to C$ (up to isomorphism) that extends $f:S\to \mathrm{Ob}(C)$.

Given categories with products $C$ and $D$, let $\mathrm{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

$$\mathrm{Prod}((\mathrm{Set}/S{)}^{\mathrm{op}},C)\simeq C^S$$\mathbf{Prod}((Set/S)^{op}, C) \simeq C^S

where the right side consists of functors $S\to C$ (where $S$ is regarded as a discrete category) and natural transformations between them.

Corollary

The category $\mathrm{Prod}((\mathrm{Set}/S{)}^{\mathrm{op}},\mathrm{Set})$ is isomorphic to $\mathrm{Set}/S$.

Proof

Because $\mathrm{Prod}((\mathrm{Set}/S{)}^{\mathrm{op}},\mathrm{Set})\simeq {\mathrm{Set}}^S\simeq \mathrm{Set}/S$.

Let $C$ be a locally small category with products. There is a Yoneda embedding

$$y:C^{\mathrm{op}}\to \mathrm{Prod}(C,\mathrm{Set})$$y: C^{op} \to \mathbf{Prod}(C, Set)

As we just saw, the Yoneda embedding $y:\mathrm{Set}/S\to \mathrm{Prod}((\mathrm{Set}/S{)}^{\mathrm{op}},\mathrm{Set})$ is an equivalence. We may arrange that the reverse equivalence $\mathrm{Prod}((\mathrm{Set}/S{)}^{\mathrm{op}},\mathrm{Set})\to \mathrm{Set}/S$ is right adjoint to $y$, and so we denote it as $y^{*}$.

Theorem

If $C$ is a locally small category with small products and $f:S\to C$ is a functor, the coproduct-preserving functor ${\Pi }^{\mathrm{op}}:\mathrm{Set}/S\to C^{\mathrm{op}}$ has a right adjoint given by the composite

$$C^{\mathrm{op}}\stackrel{y}{\to }\mathrm{Prod}(C,\mathrm{Set})\stackrel{\mathrm{Prod}(\Pi ,\mathrm{Set})}{\to }\mathrm{Prod}((\mathrm{Set}/S{)}^{\mathrm{op}},\mathrm{Set})\stackrel{y^{*}}{\to }\mathrm{Set}/S$$C^{op} \stackrel{y}\to \mathbf{Prod}(C, Set) \stackrel{\mathbf{Prod}(\Pi, Set)}{\to} \mathbf{Prod}((Set/S)^{op}, Set) \stackrel{y^*}{\to} Set/S

Proof

Let $g:X\to S$ be an object of $\mathrm{Set}/S$ and $c$ an object of $C$. We have the following natural bijections between sets of morphisms:

$$\begin{array}{ccc}{\Pi }^{\mathrm{op}}(g:X\to S)\to c& & \mathrm{in}{C}^{\mathrm{op}}\\ c\to \Pi (g:X\to S)& & \mathrm{in}C\\ y(g:X\to S)\to {\mathrm{hom}}_C(c,\Pi -)& & \mathrm{in}\mathrm{Prod}((\mathrm{Set}/S{)}^{\mathrm{op}},\mathrm{Set})\\ (g:X\to S)\to y^{*}{\mathrm{hom}}_C(c,\Pi -)& & \mathrm{in}\mathrm{Set}/S\end{array}$$\array{ \Pi^{op}(g: X \to S) \to c & & in C^{op}\\ c \to \Pi(g: X \to S) & & in C\\ y(g: X \to S) \to \hom_C(c, \Pi-) & & in \mathbf{Prod}((Set/S)^{op}, Set)\\ (g: X \to S) \to y^* \hom_C(c, \Pi-) & & in Set/S }

where we get to the third line by the Yoneda lemma. This proves the theorem.

Corollary

Under the hypotheses of the previous theorem, the product-preserving functor $\Pi :(\mathrm{Set}/S{)}^{\mathrm{op}}\to C$ is a right adjoint. In particular, it preserves all limits, not just products.

Free product-completions of categories

It will be convenient to consider first the coproduct-cocompletion; then the product-completion is obtained by dualizing.

Explicit construction

Let $C$ be a small category. We may construct the free category with coproducts generated by $C$ directly as follows:

• The objects of $\mathrm{Coprod}(C)$ are those of $\mathrm{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 $\varphi :X\to Y$ together with an $X$-indexed collection of morphisms of $C$ of the form ${\Phi }_x:f(x)\to g(\varphi (x))$.

The data of a morphism may be exhibited as a 2-cell of the form

$$\begin{array}{ccc}X& \stackrel{\varphi }{\to }& Y\\ 1_X\downarrow & \stackrel{\Phi }{\Rightarrow }& \downarrow g\\ X& \underset{f}{\to }& C\end{array}$$\array{ X & \stackrel{\phi}{\to} & Y \\ \mathllap{1_X} \downarrow & \stackrel{\Phi}{\Rightarrow} & \downarrow \mathrlap{g} \\ X & \underset{f}{\to} & C }

Coproducts of objects in $\mathrm{Coprod}(C)$ are computed just as they are in $\mathrm{Set}/C_0$. Each $f:X\to C_0$ is then a formal coproduct ${\sum }_{x}f(x)$, and a morphism $(\varphi ,\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

$$f(x)\stackrel{{\Phi }_x}{\to }g(y)\stackrel{i_y)}{\to }\sum _{y\in Y}g(y)$$f(x) \stackrel{\Phi_x}{\to} g(y) \stackrel{i_y)}{\to} \sum_{y \in Y} g(y)

where $y=\varphi (x)$. The proof of the universal property of $\mathrm{Coprod}(C)$ as coproduct cocompletion is then obvious.

As Kleisli construction

Another light on this construction comes from seeing the free coproduct-cocompletion $\mathrm{Coprod}(C)$ as sitting inside the free cocompletion ${\mathrm{Set}}^{C^{\mathrm{op}}}$. First, we have a Yoneda mapping

$$C_0\to {\mathrm{Set}}^{C^{\mathrm{op}}}:c\mapsto \mathrm{hom}(-,c)$$C_0 \to Set^{C^{op}}: c \mapsto \hom(-, c)

This induces a coproduct-preserving functor $\mathrm{Set}/C_0\to {\mathrm{Set}}^{C^{\mathrm{op}}}$, which takes an object $g:Y\to C_0$ to the presheaf

$$\sum _{y\in Y}{\mathrm{hom}}_C(-,g(y))$$\sum_{y \in Y} \hom_C(-, g(y))

By the preceding theorem, this functor has a right adjoint. The right adjoint is simply described: it is the evident underlying functor

$${\mathrm{Set}}^{C^{\mathrm{op}}}\to \mathrm{Set}/C_0$$Set^{C^{op}} \to Set/C_0

taking a presheaf $F:C^{\mathrm{op}}\to \mathrm{Set}$ to the $C_0$-indexed set where the fiber over $c\in C_0$ is $F(c)$.

Proof

As is well-known, this underlying functor ${\mathrm{Set}}^{C^{\mathrm{op}}}\to \mathrm{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

$$\sum _{y\in Y}{\mathrm{hom}}_C(c,g(y))$$\sum_{y \in Y} \hom_C(c, g(y))

In other words, the left adjoint to the underlying functor is the coproduct-preserving functor that takes $g:Y\to C_0$ to

$$\sum _{y\in Y}\mathrm{hom}(-,g(y))$$\sum_{y \in Y} \hom(-, g(y))

as described above.

Notice that $M_C(g)$ is given by the top horizontal composite

$$\begin{array}{ccccc}P& \to & C_1& \stackrel{dom}{\to }& C_0\\ \downarrow & & \downarrow cod& & \\ Y& \underset{g}{\to }& C_0& & \end{array}$$\array{ P & \to & C_1 & \stackrel{\dom}{\to} & C_0 \\ \downarrow & & \downarrow \mathrlap{\cod} & & \\ Y & \underset{g}{\to} & C_0 & & }

where the square is a pullback.

Theorem

The free coproduct-cocompletion of $C$ is the Kleisli category of the monad $M_C:\mathrm{Set}/C_0\to \mathrm{Set}/C_0$.

Proof

Let $f:X\to C_0$ and $g:Y\to C_0$ be two objects of $\mathrm{Kl}(M_C)$. A morphism from $f$ to $g$ in $\mathrm{Kl}(M_C)$ is a morphism from $f$ to $M_C(g)$ in $\mathrm{Set}/C_0$, in other words a map $h:X\to P$ making the following diagram commute:

$$\begin{array}{ccccc}X& \stackrel{1_X}{\to }& X& & \\ h\downarrow & & & \searrow f\\ P& \to & C_1& \stackrel{dom}{\to }& C_0\\ \downarrow & & \downarrow cod& & \\ Y& \underset{g}{\to }& C_0& & \end{array}$$\array{ X & \stackrel{1_X}{\to} & X & & \\ h \downarrow & & & \searrow \mathrlap{f} \\ P & \to & C_1 & \stackrel{\dom}{\to} & C_0 \\ \downarrow & & \downarrow \mathrlap{\cod} & & \\ Y & \underset{g}{\to} & C_0 & & }

Since $P$ is the pullback, the map $h$ is given by maps $\varphi :X\to Y$, $\Phi :X\to C_1$ with $\Phi (x):f(x)\to g(\varphi (x))$ for each $x\in X$. But this is how a morphism from $f$ to $g$ was described in the explicit construction of $\mathrm{Coprod}(C)$.

Example: $\mathrm{Subset}$

We calculate the free coproduct completion of the interval category $2=(0\to 1)$, and record some properties of this category.

According to theorem 3, this is the Kleisli category of the monad on $\mathrm{Set}/\{0,1\}$ corresponding to the monadic functor ${\mathrm{Set}}^{2^{\mathrm{op}}}\to \mathrm{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 $2$ given by the inclusion $X_1\hookrightarrow X_0+X_1$.

Thus the free coproduct completion of $2$ is equivalent to the category $\mathrm{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 $2$ (so that it is a reflective subcategory of ${\mathrm{Set}}^{2^{\mathrm{op}}}$). The reflection takes an object $f:X\to Y$ to the pair $(\mathrm{Im}(f),Y)$.

In particular, $\mathrm{Subset}$ is complete and cocomplete and cartesian closed. Limits are formed as they are in ${\mathrm{Set}}^{2^{\mathrm{op}}}$ (that is, objectwise). As are exponentials, since $\mathrm{Subset}$ is actually an exponential ideal in ${\mathrm{Set}}^{2^{\mathrm{op}}}$. Naturally, coproducts are formed as they are in the presheaf category since $\mathrm{Subset}$ is the coproduct completion; coequalizers are constructed by forming them in the presheaf category and then reflecting back into $\mathrm{Subset}$.

Categories enriched in $\mathrm{Subset}$ are also called M-categories.

Algebraic theory of a category

The free product-completion of $C$ is obtained by dualization:

$$\mathrm{Prod}(C)=\mathrm{Coprod}(C^{\mathrm{op}}{)}^{\mathrm{op}}=\mathrm{Kl}(M_{C^{\mathrm{op}}}{)}^{\mathrm{op}}$$Prod(C) = Coprod(C^{op})^{op} = Kl(M_{C^{op}})^{op}

Here $M=M_{C^{\mathrm{op}}}$ is the monad on $\mathrm{Set}/C_0$ whose algebras are functors $C\to \mathrm{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 $\mathrm{Kl}(M{)}^{\mathrm{op}}$, in other words the product-completion of $C$. Indeed, the category of models of $\mathrm{Kl}(M{)}^{\mathrm{op}}$ is

$$\mathrm{Prod}(\mathrm{Kl}(M{)}^{\mathrm{op}},\mathrm{Set})\simeq \mathrm{Prod}(\mathrm{Prod}(C),\mathrm{Set})\simeq {\mathrm{Set}}^C$$\mathbf{Prod}(Kl(M)^{op}, Set) \simeq \mathbf{Prod}(Prod(C), Set) \simeq Set^C

by the universal property of $\mathrm{Prod}(C)$.

KZ property

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 $\mathrm{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 $\varphi :X\to Y$ together with an $X$-indexed collection of morphisms ${\Phi }_x:f(x)\to g(\varphi (x))$. The hom-sets are clearly small.

To be continued…

Free cartesian category on a signature

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 $\mathrm{Term}(S,F)$.

As before, the objects of $\mathrm{Term}(S,F)$ are product types: elements of $S^{*}$. Morphisms from a type $T:[m]\to S$ to a type $T\prime :[n]\to S$ are, in the language of the preceding section, $n$-tuples of normal terms $(t_1,\dots ,t_n)$ where each $t_i$ has arity $T\to T\prime (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:

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

$$Mc\stackrel{f}{\leftarrow }x\stackrel{g}{\to }d$$M c \stackrel{f}{\leftarrow} x \stackrel{g}{\to} d

$M$-spans are composed by consideration of a pullback

$$\begin{array}{ccccccccccc}& & & & & & x\circ y& & & & \\ & & & & & \swarrow & & \searrow & & & \\ & & & & My& & & & x& & \\ & & & {}^{Mh}\swarrow & & {\searrow }^{Mk}& & {}^{Mf}\swarrow & & {\searrow }^g& \\ Mb& \stackrel{m_b}{\leftarrow }& MMb& & & & Mc& & & & d\end{array}$$\array{ & & & & & & x \circ y & & & & \\ & & & & & \swarrow & & \searrow & & & \\ & & & & M y & & & & x & & \\ & & & ^\mathllap{M h} \swarrow & & \searrow ^\mathrlap{M k} & & ^\mathllap{M f} \swarrow & & \searrow ^\mathrlap{g} & \\ M b & \stackrel{m_b}{\leftarrow} & M M b & & & & M c & & & & d }

where $m:MM\to M$ is the multiplication on the monad $M$. Under this composition, the $M$-spans are 1-cells of a bicategory $M$-$\mathrm{Span}$.

In the case where $M$ is the free monoid monad acting on $\mathrm{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$-$\mathrm{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 $\mathrm{Set}/S$ which takes an $S$-indexed set $X_s$ to

$$P(X{)}_s=\sum _{T\in S^{*}}\sum _{f:T\to s}\prod _{s\prime \in S}{X}_{s\prime }^{T_{s\prime }}$$P(X)_s = \sum_{T \in S^\ast} \sum_{f: T \to s} \prod_{s' \in S} X_{s'}^{T_{s'}}

($f\in F$). However it is named, the underlying multigraph of the free multicategory generated by a multigraph $F$ can be described as

$$\begin{array}{ccccc}& & \mathrm{Tree}(F)& & \\ & {}^{\mathrm{in}}\swarrow & & {\searrow }^{\mathrm{out}}& \\ S^{*}& & & & S\end{array}$$\array{ & & Tree(F) & & \\ & ^\mathllap{in} \swarrow & & \searrow ^\mathrlap{out} & \\ S^\ast & & & & S }

where $\mathrm{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 $\mathrm{in}(t)\in S^{*}$, and the label of the “root” edge gives an element $\mathrm{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 $\mathrm{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 $\mathrm{Pro}(S,F)$ are elements of $S^{*}$. The morphisms of $\mathrm{Pro}(S,F)$ could be described as ”$F$-labeled forests”. Formally, the underlying span of $\mathrm{Pro}(S,F)$ is

$$S^{*}\stackrel{m_S}{\leftarrow }{S}^{**}\stackrel{{\mathrm{in}}^{*}}{\leftarrow }\mathrm{Tree}(F{)}^{*}\stackrel{{\mathrm{out}}^{*}}{\to }{S}^{*}$$S^\ast \stackrel{m_S}{\leftarrow} S^{\ast\ast} \stackrel{in^\ast}{\leftarrow} Tree(F)^\ast \stackrel{out^\ast}{\to} S^\ast

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 $\mathrm{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 $\mathrm{Pro}(S,F)\circ \mathrm{Prod}(S)$ be the composite of the two spans

$$\begin{array}{ccccccccc}& & \mathrm{Prod}(S)& & & & \mathrm{Pro}(S,F)& & \\ & {}^{\mathrm{dom}}\swarrow & & {\searrow }^{\mathrm{cod}}& & {}^{\mathrm{in}}\swarrow & & {\searrow }^{\mathrm{out}}& \\ S^{*}& & & & S^{*}& & & & S^{*}\end{array}$$\array{ & & Prod(S) & & & & Pro(S, F) & & \\ & ^\mathllap{dom} \swarrow & & \searrow ^\mathrlap{cod} & & ^\mathllap{in} \swarrow & & \searrow ^\mathrlap{out} & \\ S^\ast & & & & S^\ast & & & & S^\ast }

Then, in the first place, $\mathrm{Pro}(S,F)\circ \mathrm{Prod}(S)$ carries a canonical category structure. The reason is that, viewing $\mathrm{Prod}(S)$ and $\mathrm{Pro}(S,F)$ as monads in the bicategory of spans, there is a canonical distributive law

$$\theta :\mathrm{Prod}(S)\circ \mathrm{Pro}(S,F)\to \mathrm{Pro}(S,F)\circ \mathrm{Prod}(S)$$\theta: Prod(S) \circ Pro(S, F) \to Pro(S, F) \circ Prod(S)

(here $\mathrm{Pro}(S,F)$ can be replaced by any pro over $S$). The idea is that the distributive law $\theta$ maps an element of $\mathrm{Prod}(S)\circ \mathrm{Pro}(S,F)$, which is a pair of arrows

$$T\stackrel{f}{\to }T\prime \stackrel{d}{\to }T″$$T \stackrel{f}{\to} T' \stackrel{d}{\to} T''

with $f$ an arrow of $\mathrm{Pro}(S,F)$ and $d$ an arrow of $\mathrm{Prod}(S)$, to a pair of arrows in $\mathrm{Pro}(S,F)\circ \mathrm{Prod}(S)$ whose precise form is dictated by a naturality requirement in $d$. For example, if $d={\delta }_T\prime :T\prime \to T\prime \otimes T\prime$, then

$$\theta (f,{\delta }_T\prime )=(T\stackrel{{\delta }_T}{\to }T\otimes T\stackrel{f\otimes f}{\to }T\prime \otimes T\prime )$$\theta(f, \delta_T') = (T \stackrel{\delta_T}{\to} T \otimes T \stackrel{f \otimes f}{\to} T' \otimes T')

Using this distributive law, the composite of the monads $\mathrm{Prod}(S)$ and $\mathrm{Pro}(S,F)$ is another monad in the bicategory of spans, and therefore a category with set of objects $S^{*}$.

The same trick works for other doctrines over the doctrine of monoidal categories. For example, if $\mathrm{Perm}(S)$ is the free symmetric (strict) monoidal category generated by $S$, regarded as a span from $S^{*}$ to $S^{*}$, then there is a distributive law $\mathrm{Perm}(S)\circ \mathrm{Pro}(S,F)\to \mathrm{Pro}(S,F)\circ \mathrm{Perm}(S)$. Similarly with “symmetric monoidal” replaced with “braided monoidal”.

Definition

$\mathrm{Term}(S,F)≔\mathrm{Pro}(S,F)\circ \mathrm{Prod}(S)$, regarded as a cartesian category with product structure inherited from $\mathrm{Prod}(S)$, meaning that

$$\mathrm{Prod}(S)\cong {\mathrm{id}}_{S^{*}}\circ \mathrm{Prod}(S)\stackrel{u\circ 1}{\to }\mathrm{Pro}(S,F)\circ \mathrm{Prod}(S)$$Prod(S) \cong id_{S^\ast} \circ Prod(S) \stackrel{u \circ 1}{\to} Pro(S, F) \circ Prod(S)

is a product-preserving functor, where $u$ is the unit of the monad $\mathrm{Pro}(S,F)$.

More explicitly, the tensor product $⨂$ on $\mathrm{Term}(S,F)$ is a cartesian product provided that there are natural transformations $\delta :\mathrm{id}\to \otimes \Delta$, $\epsilon :\mathrm{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 $\mathrm{Prod}(S)$.

Note that this abstract description of $\mathrm{Term}(S,F)$ is identical to that given by the syntax of normal terms. The “bureaucracy of variables” is here organized into two departments, $\mathrm{Prod}(S)$ and $\mathrm{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 $\mathrm{Term}(S,F)$ is factorized into a generalized diagonal map followed by an $F$-labeled forest.)

Another name for $\mathrm{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$”.

Theorem

$\mathrm{Term}(S,F)$ is the free category with products generated by the multigraph $F$ over $S$.

Proof

$\mathrm{Tree}(S,F)$ is the free multicategory generated by the multigraph $F$ over $S$, and $\mathrm{Pro}(S,F)$ is the free monoidal category generated by the multicategory $\mathrm{Tree}(S,F)$. Therefore $\mathrm{Pro}(S,F)$ is the free monoidal category generated by the multigraph $F$. It remains to show that the monoidal inclusion

$$\mathrm{Pro}(S,F)\cong \mathrm{Pro}(S,F)\circ {\mathrm{id}}_{S^{*}}\stackrel{1\circ u}{\to }\mathrm{Pro}(S,F)\circ \mathrm{Prod}(S)$$Pro(S, F) \cong Pro(S, F) \circ id_{S^\ast} \stackrel{1 \circ u}{\to} Pro(S, F) \circ Prod(S)

is universal among monoidal functors $X:\mathrm{Pro}(S,F)\to C$ to cartesian monoidal categories $C$.

There is of course a product-preserving functor $\mathrm{Prod}(S)\to C$ compatible with the restriction $S^{*}\hookrightarrow \mathrm{Pro}(S,F)\stackrel{X}{\to }C$. At the level of spans, this gives a composable pair of span morphisms

$$\begin{array}{ccccccccc}{S}^{*}& \stackrel{dom}{\leftarrow }& \mathrm{Prod}(S)& \stackrel{cod}{\to }& S^{*}& \stackrel{\mathrm{in}}{\leftarrow }& \mathrm{Pro}(S,F)& \stackrel{\mathrm{out}}{\to }& S^{*}\\ \downarrow & & \downarrow & & \downarrow & & \downarrow & & \downarrow \\ C_0& \underset{d_0}{\leftarrow }& C_1& \underset{d_1}{\to }& C_0& \underset{d_0}{\leftarrow }& C_1& \underset{d_1}{\to }& C_0\end{array}$$\array{ S^\ast & \stackrel{\dom}{\leftarrow} & Prod(S) & \stackrel{\cod}{\to} & S^\ast & \stackrel{in}{\leftarrow} & Pro(S, F) & \stackrel{out}{\to} & S^\ast \\ \downarrow & & \downarrow & & \downarrow & & \downarrow & & \downarrow \\ C_0 & \underset{d_0}{\leftarrow} & C_1 & \underset{d_1}{\to} & C_0 & \underset{d_0}{\leftarrow} & C_1 & \underset{d_1}{\to} & C_0 }

which we then compose with the span morphism $m:C_1\circ C_1\to C_1$ given by composition in $C$:

$$\mathrm{Pro}(S,F)\circ \mathrm{Prod}(S)\to C_1\circ C_1\stackrel{m}{\to }{C}_1$$Pro(S, F) \circ Prod(S) \to C_1 \circ C_1 \stackrel{m}{\to} C_1

This gives a morphism between underlying spans, $\mathrm{Term}(S,F)\to C$. This is functorial (i.e., is a morphism of monads in $\mathrm{Span}$) because both $\mathrm{Prod}(S)\to C$ and $\mathrm{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 $\mathrm{Term}(S,F)\to C$ is product-preserving, because $\mathrm{Prod}(S)\to C$ is product-preserving. The uniqueness of the product-preserving extension $\mathrm{Term}(S,F)\to C$ is clear since the subcategories $\mathrm{Prod}(S)$ and $\mathrm{Pro}(S,F)$ together generate $\mathrm{Term}(S,F)$.