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 SS. This is, by definition, a category with small products, Prod(S)Prod(S), equipped with a function i:SOb(Prod(S))i \,\colon\, S \to Ob(Prod(S)) with the following universal property: given a category CC with small products and a function f:SOb(C)f \,\colon\, S \to Ob(C), there exists up to (unique) isomorphism a unique product-preserving functor Π:Prod(S)C\Pi \,\colon\, Prod(S) \to C such that f=Ob(Π)if = Ob(\Pi) \circ i.

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

Each object n:NSn: N \to S of (Set/S) op(Set/S)^{op} can be regarded as a formal product sSx s n s\prod_{s \in S} x_{s}^{n_s} where SS indexes a set of variables x sx_s and n s=n 1(s)n_s = n^{-1}(s) is the (cardinality of the) fiber over SS. Therefore the following theorem comes as no surprise.


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


Let CC be a category with small products. Given f:SOb(C)f: S \to Ob(C), the functor Π:(Set/S) opC\Pi: (Set/S)^{op} \to C is defined on the object-level: n:NSn: N \to S is sent to sSf(s) n s\prod_{s \in S} f(s)^{n_s} in CC. In addition, a morphism from m:MSm: M \to S to n:NSn: N \to S in (Set/S) op(Set/S)^{op} is a function ϕ:NM\phi: N \to M that satisfies mϕ=nm \circ \phi = n; this in turn consists of a collection of functions ϕ s:n sm s\phi_s: n_s \to m_s indexed by elements sSs \in S, and each such function induces a morphism

f(s) ϕ s:f(s) m sf(s) n sf(s)^{\phi_s}: f(s)^{m_s} \to f(s)^{n_s}

in CC, uniquely specified by declaring the i thi^{th} component of this morphism for in si \in n_s to be given by

f(s) m sproj ϕ s(i)f(s)f(s)^{m_s} \stackrel{proj_{\phi_s(i)}}{\to} f(s)

Given a morphism ϕ\phi of (Set/S) op(Set/S)^{op}, define Π(ϕ)\Pi(\phi) by

Π(ϕ)=f(s) ϕ s sS: sSf(s) m s sSf(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 (Set/S) opC(Set/S)^{op} \to C (up to isomorphism) that extends f:SOb(C)f: S \to Ob(C).

Given categories with products CC and DD, let Prod(C,D)\mathbf{Prod}(C, D) denote the category of product-preserving functors F:CDF: C \to D and natural transformations between them. By the preceding theorem, there is an equivalence

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

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


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


Because Prod((Set/S) op,Set)Set SSet/S\mathbf{Prod}((Set/S)^{op}, Set) \simeq Set^S \simeq Set/S.

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

y:C opProd(C,Set) y \;\colon\; C^{op} \to \mathbf{Prod}(C, Set)

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


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

C opyProd(C,Set)Prod(Π,Set)Prod((Set/S) op,Set)y *Set/SC^{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

Let g:XSg: X \to S be an object of Set/SSet/S and cc an object of CC. We have the following natural bijections between sets of morphisms:

Π op(g:XS)c inC op cΠ(g:XS) inC y(g:XS)hom C(c,Π) inProd((Set/S) op,Set) (g:XS)y *hom C(c,Π) inSet/S\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.


Under the hypotheses of the previous theorem, the product-preserving functor Π:(Set/S) opC\Pi: (Set/S)^{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 CC be a small category. We may construct the free category with coproducts generated by CC directly as follows:

  • The objects of Coprod(C)Coprod(C) are those of Set/C 0Set/C_0, where C 0C_0 is the set of objects.

  • A morphism (say from f:XC 0f: X \to C_0 to g:YC 0g: Y \to C_0) is given by a function ϕ:XY\phi: X \to Y together with an XX-indexed collection of morphisms of CC of the form Φ x:f(x)g(ϕ(x))\Phi_x: f(x) \to g(\phi(x)).

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

X ϕ Y 1 X Φ g X f C\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 Coprod(C)Coprod(C) are computed just as they are in Set/C 0Set/C_0. Each f:XC 0f: X \to C_0 is then a formal coproduct xf(x)\sum_x f(x), and a morphism (ϕ,Φ): xXf(x) yYg(y)(\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) xf(x)i_x: f(x) \to \sum_x f(x), which in turn are given by composites

f(x)Φ xg(y)i y) yYg(y)f(x) \stackrel{\Phi_x}{\to} g(y) \stackrel{i_y)}{\to} \sum_{y \in Y} g(y)

where y=ϕ(x)y = \phi(x). The proof of the universal property of Coprod(C)Coprod(C) as coproduct cocompletion is then obvious.

As Kleisli construction

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

C 0Set C op:chom(,c)C_0 \to Set^{C^{op}} \;\colon\; c \mapsto \hom(-, c)

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

yYhom 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

Set C opSet/C 0Set^{C^{op}} \to Set/C_0

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


As is well-known, this underlying functor Set C opSet/C 0Set^{C^{op}} \to Set/C_0 is monadic; the monad M CM_C takes an object g:YC 0g: Y \to C_0 to the object whose fiber over cc is the set

yYhom 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:YC 0g: Y \to C_0 to

yYhom(,g(y))\sum_{y \in Y} \hom(-, g(y))

as described above.

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

P C 1 dom C 0 cod Y g C 0 \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.


The free coproduct-cocompletion of CC is the Kleisli category of the monad M C:Set/C 0Set/C 0M_C: Set/C_0 \to Set/C_0.


Let f:XC 0f: X \to C_0 and g:YC 0g: Y \to C_0 be two objects of Kl(M C)Kl(M_C). A morphism from ff to gg in Kl(M C)Kl(M_C) is a morphism from ff to M C(g)M_C(g) in Set/C 0Set/C_0, in other words a map h:XPh: X \to P making the following diagram commute:

X 1 X X h f P C 1 dom C 0 cod Y g C 0 \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 PP is the pullback, the map hh is given by maps ϕ:XY\phi: X \to Y, Φ:XC 1\Phi: X \to C_1 with Φ(x):f(x)g(ϕ(x))\Phi(x): f(x) \to g(\phi(x)) for each xXx \in X. But this is how a morphism from ff to gg was described in the explicit construction of Coprod(C)Coprod(C).

Example: SubsetSubset

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

According to theorem , this is the Kleisli category of the monad on Set/{0,1}Set/\{0, 1\} corresponding to the monadic functor Set 2 opSet/{0,1}Set^{\mathbf{2}^{op}} \to Set/\{0, 1\}. This monad takes a pair of sets (X 1,X 0)(X_1, X_0) to (X 1,X 0+X 1)(X_1, X_0 + X_1); the algebra structure of the free algebra (X 1,X 0+X 1)(X_1, X_0 + X_1) is the structure of presheaf over 2\mathbf{2} given by the inclusion X 1X 0+X 1X_1 \hookrightarrow X_0 + X_1.

Thus the free coproduct completion of 2\mathbf{2} is equivalent to the category SubsetSubset who objects are pairs of sets (A,X)(A, X) where AA is a subset of XX; morphisms (A,X)(B,Y)(A, X) \to (B, Y) are functions f:XYf: X \to Y which carry AA into BB.

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\mathbf{2} (so that it is a reflective subcategory of Set 2 opSet^{\mathbf{2}^{op}}). The reflection takes an object f:XYf: X \to Y to the pair (Im(f),Y)(Im(f), Y).

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

Categories enriched in SubsetSubset are also called M-categories.

Algebraic theory of a category

The free product-completion of CC is obtained by dualization:

Prod(C)=Coprod(C op) op=Kl(M C op) opProd(C) = Coprod(C^{op})^{op} = Kl(M_{C^{op}})^{op}

Here M=M C opM = M_{C^{op}} is the monad on Set/C 0Set/C_0 whose algebras are functors CSetC \to Set. This functor category is the category of models of a simple multi-sorted algebraic theory, where the set of sorts is C 0C_0 and each morphism f:cdf: c \to d is regarded as an unary operation. According to the entry algebraic theory, the corresponding Lawvere theory is just Kl(M) opKl(M)^{op}, in other words the product-completion of CC. Indeed, the category of models of Kl(M) opKl(M)^{op} is

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

by the universal property of Prod(C)Prod(C).

KZ property

There is no foundational difficulty in forming the free small coproduct-cocompletion of any locally small category CC (any more than forming the free cocompletion with respect to small limits). An object of Coprod(C)Coprod(C) is a set XX together with a function f:XC 0f: X \to C_0. A morphism from f:XC 0f: X \to C_0 to g:YC 0g: Y \to C_0 consists of a function ϕ:XY\phi: X \to Y together with an XX-indexed collection of morphisms Φ x:f(x)g(ϕ(x))\Phi_x: f(x) \to g(\phi(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 FF over SS. We denote this free category with products as Term(S,F)Term(S, F).

As before, the objects of Term(S,F)Term(S, F) are product types: elements of S *S^\ast. Morphisms from a type T:[m]ST: [m] \to S to a type T:[n]ST': [n] \to S are, in the language of the preceding section, nn-tuples of normal terms (t 1,,t n)(t_1, \ldots, t_n) where each t it_i has arity TT(i)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 MM be a cartesian monad acting on a finitely complete category CC. An MM-span in CC from cc to dd is a span of the form

McfxgdM c \stackrel{f}{\leftarrow} x \stackrel{g}{\to} d

MM-spans are composed by consideration of a pullback

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

where m:MMMm: M M \to M is the multiplication on the monad MM. Under this composition, the MM-spans are 1-cells of a bicategory MM-SpanSpan.

In the case where MM is the free monoid monad acting on SetSet, an MM-span from a set SS to SS is the same as a multigraph over SS. A monad on SS in the bicategory MM-SpanSpan is a multicategory over SS. We are especially interested in the free multicategory generated from a multigraph over SS.

The free multicategory construction has other names and descriptions. We could also call it the free nonpermutative SS-sorted operad generated by a set of SS-typed function symbols. The apex of its underlying span, together with its map to SS, can also be referred to as the initial algebra for the polynomial endofunctor PP on Set/SSet/S which takes an SS-indexed set X sX_s to

P(X) s= TS * f:Ts sSX s T sP(X)_s = \sum_{T \in S^\ast} \sum_{f: T \to s} \prod_{s' \in S} X_{s'}^{T_{s'}}

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

Tree(F) in out S * S\array{ & & Tree(F) & & \\ & ^\mathllap{in} \swarrow & & \searrow ^\mathrlap{out} & \\ S^\ast & & & & S }

where Tree(F)Tree(F) is the set of FF-labeled planar trees. This means that

  • Nodes of a planar tree are labeled by elements f:Tsf: T \to s of FF;

  • Edges of that planar tree are labeled by sorts ss, such that the list of labels of incoming edges at a node f:Tsf: T \to s is the word TT, and the outgoing edge is labeled ss.

The list of labels of “leaves” of an FF-labeled tree tt (edges that are not outgoing edges of any node) gives an element in(t)S *in(t) \in S^\ast, and the label of the “root” edge gives an element out(t)Sout(t) \in S. Notice that FF-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)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)Pro(S, F) are elements of S *S^\ast. The morphisms of Pro(S,F)Pro(S, F) could be described as “FF-labeled forests”. Formally, the underlying span of Pro(S,F)Pro(S, F) is

S *m SS **in *Tree(F) *out *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 Pro(S,F)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)Prod(S)Pro(S, F) \circ Prod(S) be the composite of the two spans

Prod(S) Pro(S,F) dom cod in out S * S * S *\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, Pro(S,F)Prod(S)Pro(S, F) \circ Prod(S) carries a canonical category structure. The reason is that, viewing Prod(S)Prod(S) and Pro(S,F)Pro(S, F) as monads in the bicategory of spans, there is a canonical distributive law

θ:Prod(S)Pro(S,F)Pro(S,F)Prod(S)\theta: Prod(S) \circ Pro(S, F) \to Pro(S, F) \circ Prod(S)

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

TfTdTT \stackrel{f}{\to} T' \stackrel{d}{\to} T''

with ff an arrow of Pro(S,F)Pro(S, F) and dd an arrow of Prod(S)Prod(S), to a pair of arrows in Pro(S,F)Prod(S)Pro(S, F) \circ Prod(S) whose precise form is dictated by a naturality requirement in dd. For example, if d=δ T:TTTd = \delta_T': T' \to T' \otimes T', then

θ(f,δ T)=(Tδ TTTffTT)\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 Prod(S)Prod(S) and Pro(S,F)Pro(S, F) is another monad in the bicategory of spans, and therefore a category with set of objects S *S^\ast.

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


Term(S,F)Pro(S,F)Prod(S)Term(S, F) \coloneqq Pro(S, F) \circ Prod(S), regarded as a cartesian category with product structure inherited from Prod(S)Prod(S), meaning that

Prod(S)id S *Prod(S)u1Pro(S,F)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 uu is the unit of the monad Pro(S,F)Pro(S, F).

More explicitly, the tensor product \bigotimes on Term(S,F)Term(S, F) is a cartesian product provided that there are natural transformations δ:idΔ\delta: id \to \otimes \Delta, ε:ide!\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)Prod(S).

Note that this abstract description of Term(S,F)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)Prod(S) and Pro(S,F)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)Term(S, F) is factorized into a generalized diagonal map followed by an FF-labeled forest.)

Another name for Term(S,F)Term(S, F) is “term algebra”, and yet another name for it is “the free SS-sorted Lawvere theory generated by a set of SS-sorted operation symbols FF”.


Term(S,F)Term(S, F) is the free category with products generated by the multigraph FF over SS.


Tree(S,F)Tree(S, F) is the free multicategory generated by the multigraph FF over SS, and Pro(S,F)Pro(S, F) is the free monoidal category generated by the multicategory Tree(S,F)Tree(S, F). Therefore Pro(S,F)Pro(S, F) is the free monoidal category generated by the multigraph FF. It remains to show that the monoidal inclusion

Pro(S,F)Pro(S,F)id S *1uPro(S,F)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:Pro(S,F)CX: Pro(S, F) \to C to cartesian monoidal categories CC.

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

S * dom Prod(S) cod S * in Pro(S,F) out S * C 0 d 0 C 1 d 1 C 0 d 0 C 1 d 1 C 0\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 1C 1C 1m: C_1 \circ C_1 \to C_1 given by composition in CC:

Pro(S,F)Prod(S)C 1C 1mC 1Pro(S, F) \circ Prod(S) \to C_1 \circ C_1 \stackrel{m}{\to} C_1

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

Last revised on June 5, 2022 at 19:16:58. See the history of this page for a list of all contributions to it.