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 . This by definition is a category with small products, , equipped with a function with the following universal property: given a category with small products and a function , there exists up to (unique) isomorphism a unique product-preserving functor such that .
Each object of can be regarded as a formal product where indexes a set of variables and is the (cardinality of the) fiber over . Therefore the following theorem comes as no surprise.
together with is the free category with small products generated by .
Let be a category with small products. Given , the functor is defined on the object-level: is sent to in . In addition, a morphism from to in is a function that satisfies ; this in turn consists of a collection of functions indexed by elements , and each such function induces a morphism
in , uniquely specified by declaring the component of this morphism for to be given by
Given a morphism of , define by
The functor is the unique product-preserving functor (up to isomorphism) that extends .
Given categories with products and , let denote the category of product-preserving functors and natural transformations between them. By the preceding theorem, there is an equivalence
where the right side consists of functors (where is regarded as a discrete category) and natural transformations between them.
The category is isomorphic to .
Let be a locally small category with products. There is a Yoneda embedding
As we just saw, the Yoneda embedding is an equivalence. We may arrange that the reverse equivalence is right adjoint to , and so we denote it as .
If is a locally small category with small products and is a functor, the coproduct-preserving functor has a right adjoint given by the composite
Let be an object of and an object of . 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 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 be a small category. We may construct the free category with coproducts generated by directly as follows:
The objects of are those of , where is the set of objects.
A morphism (say from to ) is given by a function together with an -indexed collection of morphisms of of the form .
The data of a morphism may be exhibited as a 2-cell of the form
Coproducts of objects in are computed just as they are in . Each is then a formal coproduct , and a morphism is uniquely determined by its restrictions along the coprojections , which in turn are given by composites
where . The proof of the universal property of as coproduct cocompletion is then obvious.
Another light on this construction comes from seeing the free coproduct-cocompletion as sitting inside the free cocompletion . First, we have a Yoneda mapping
This induces a coproduct-preserving functor , which takes an object 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 to the -indexed set where the fiber over is .
As is well-known, this underlying functor is monadic; the monad takes an object to the object whose fiber over is the set
In other words, the left adjoint to the underlying functor is the coproduct-preserving functor that takes to
as described above.
Notice that is given by the top horizontal composite
where the square is a pullback.
The free coproduct-cocompletion of is the Kleisli category of the monad .
Let and be two objects of . A morphism from to in is a morphism from to in , in other words a map making the following diagram commute:
Since is the pullback, the map is given by maps , with for each . But this is how a morphism from to was described in the explicit construction of .
We calculate the free coproduct completion of the interval category , and record some properties of this category.
According to theorem 3, this is the Kleisli category of the monad on corresponding to the monadic functor . This monad takes a pair of sets to ; the algebra structure of the free algebra is the structure of presheaf over given by the inclusion .
Thus the free coproduct completion of is equivalent to the category who objects are pairs of sets where is a subset of ; morphisms are functions which carry into .
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 -separated presheaves on (so that it is a reflective subcategory of ). The reflection takes an object to the pair .
In particular, is complete and cocomplete and cartesian closed. Limits are formed as they are in (that is, objectwise). As are exponentials, since is actually an exponential ideal in . Naturally, coproducts are formed as they are in the presheaf category since is the coproduct completion; coequalizers are constructed by forming them in the presheaf category and then reflecting back into .
The free product-completion of is obtained by dualization:
Here is the monad on whose algebras are functors . This functor category is the category of models of a simple multi-sorted algebraic theory, where the set of sorts is and each morphism is regarded as an unary operation. According to the entry algebraic theory, the corresponding Lawvere theory is just , in other words the product-completion of . Indeed, the category of models of is
by the universal property of .
There is no foundational difficulty in forming the free small coproduct-cocompletion of any locally small category (any more than forming the free cocompletion with respect to small limits). An object of is a set together with a function . A morphism from to consists of a function together with an -indexed collection of morphisms . 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 over . We denote this free category with products as .
As before, the objects of are product types: elements of . Morphisms from a type to a type are, in the language of the preceding section, -tuples of normal terms where each has arity . 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 -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 be a cartesian monad acting on a finitely complete category . An -span in from to is a span of the form
-spans are composed by consideration of a pullback
where is the multiplication on the monad . Under this composition, the -spans are 1-cells of a bicategory -.
In the case where is the free monoid monad acting on , an -span from a set to is the same as a multigraph over . A monad on in the bicategory - is a multicategory over . We are especially interested in the free multicategory generated from a multigraph over .
The free multicategory construction has other names and descriptions. We could also call it the free nonpermutative -sorted operad generated by a set of -typed function symbols. The apex of its underlying span, together with its map to , can also be referred to as the initial algebra for the polynomial endofunctor on which takes an -indexed set to
(). However it is named, the underlying multigraph of the free multicategory generated by a multigraph can be described as
where is the set of -labeled planar trees. This means that
Nodes of a planar tree are labeled by elements of ;
Edges of that planar tree are labeled by sorts , such that the list of labels of incoming edges at a node is the word , and the outgoing edge is labeled .
The list of labels of “leaves” of an -labeled tree (edges that are not outgoing edges of any node) gives an element , and the label of the “root” edge gives an element . Notice that -labeled trees have obvious string diagram representations.
Next, any multicategory generates a (strict monoidal) category. In the present instance, we denote this category as (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 are elements of . The morphisms of could be described as ”-labeled forests”. Formally, the underlying span of 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 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 be the composite of the two spans
Then, in the first place, carries a canonical category structure. The reason is that, viewing and as monads in the bicategory of spans, there is a canonical distributive law
(here can be replaced by any pro over ). The idea is that the distributive law maps an element of , which is a pair of arrows
with an arrow of and an arrow of , to a pair of arrows in whose precise form is dictated by a naturality requirement in . For example, if , then
Using this distributive law, the composite of the monads and is another monad in the bicategory of spans, and therefore a category with set of objects .
The same trick works for other doctrines over the doctrine of monoidal categories. For example, if is the free symmetric (strict) monoidal category generated by , regarded as a span from to , then there is a distributive law . Similarly with “symmetric monoidal” replaced with “braided monoidal”.
, regarded as a cartesian category with product structure inherited from , meaning that
is a product-preserving functor, where is the unit of the monad .
More explicitly, the tensor product on is a cartesian product provided that there are natural transformations , 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 .
Note that this abstract description of is identical to that given by the syntax of normal terms. The “bureaucracy of variables” is here organized into two departments, and , 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 is factorized into a generalized diagonal map followed by an -labeled forest.)
Another name for is “term algebra”, and yet another name for it is “the free -sorted Lawvere theory generated by a set of -sorted operation symbols ”.
is the free category with products generated by the multigraph over .
is the free multicategory generated by the multigraph over , and is the free monoidal category generated by the multicategory . Therefore is the free monoidal category generated by the multigraph . It remains to show that the monoidal inclusion
is universal among monoidal functors to cartesian monoidal categories .
There is of course a product-preserving functor compatible with the restriction . At the level of spans, this gives a composable pair of span morphisms
which we then compose with the span morphism given by composition in :
This gives a morphism between underlying spans, . This is functorial (i.e., is a morphism of monads in ) because both and are functorial, and also because the compositional equalities enforced by the distributive law are preserved: they are taken to equalities expressed by naturality of diagonal maps and projection maps in . The functor is product-preserving, because is product-preserving. The uniqueness of the product-preserving extension is clear since the subcategories and together generate .