Cartesian Closed Categories

Cartesian Closure

An adjunction can be discovered or demanded. In \(\mathbf{Set}\) it was discovered. The bijection between functions of two arguments and functions valued in function sets was already there, waiting to be recognized as \(- \times B \dashv (-)^B\). Demanding the same pattern of an arbitrary category is a strong condition, and the categories that meet it are those whose objects can hold the maps between objects of their own kind. Such a category carries an internal notion of function.

The definition asks for a right adjoint, not for a formula, so \(C^B\) is pinned down only up to isomorphism and a cartesian closed structure carries a choice of exponentials along with it. The counit of \(- \times B \dashv (-)^B\) has components \[ \operatorname{ev}_{B,C} : C^B \times B \to C , \] the evaluation maps, and by the transpose formulae the bijection of the definition, read from right to left, sends \(\bar{h} : A \to C^B\) to \(\operatorname{ev}_{B,C} \circ (\bar{h} \times 1_B)\). A map out of a product is recovered from its transpose by feeding the transpose its second argument.

Naturality in the exponent \(B\) is absent from the definition, and it need not be imposed, because it follows. Fix \(C\) and let \(g : B' \to B\) be a map. The exponential is made contravariantly functorial in the exponent by defining \(g^* : C^B \to C^{B'}\) to be the transpose of \(\operatorname{ev}_{B,C} \circ (1_{C^B} \times g)\), which is to say the unique map with \[ \operatorname{ev}_{B',C} \circ (g^* \times 1_{B'}) = \operatorname{ev}_{B,C} \circ (1_{C^B} \times g) . \] With that definition the bijection is natural in \(B\) as well.

The transposes agree. Let \(h : A \times B \to C\) with transpose \(\bar{h} : A \to C^B\). Since a map into an exponential is determined by its composite with the evaluation map, it is enough to compare the two candidates after that composition, and \[ \begin{align*} \operatorname{ev}_{B',C} \circ \big((g^* \circ \bar{h}) \times 1_{B'}\big) &= \operatorname{ev}_{B',C} \circ (g^* \times 1_{B'}) \circ (\bar{h} \times 1_{B'}) \\\\ &= \operatorname{ev}_{B,C} \circ (1_{C^B} \times g) \circ (\bar{h} \times 1_{B'}) \\\\ &= \operatorname{ev}_{B,C} \circ (\bar{h} \times 1_B) \circ (1_A \times g) \\\\ &= h \circ (1_A \times g) . \end{align*} \] The second equality is the defining property of \(g^*\), and the third holds because the product of the two maps \(\bar{h}\) and \(g\) may be formed one coordinate at a time, in either order. The last line is the image of \(h\) under precomposition with \(1_A \times g\), so \(g^* \circ \bar{h}\) is the transpose of \(h \circ (1_A \times g)\), which is exactly the naturality square in \(B\).

Sets

The category \(\mathbf{Set}\) is cartesian closed, and it is the example the definition was reverse engineered from. It has finite products, the product of sets together with a one-element set as terminal object, and the currying adjunction is the required right adjoint, with the exponential \(C^B\) the set of functions from \(B\) to \(C\). The evaluation map of the definition is the function \((h, b) \mapsto h(b)\) recorded there, so the abstract counit is the concrete act of applying a function to an argument.

Small categories

The category \(\mathbf{Cat}\) of small categories is cartesian closed, with the exponential \(\mathscr{C}^{\mathscr{B}} = [\mathscr{B}, \mathscr{C}]\) the functor category. Three things have to hold: that \(\mathbf{Cat}\) has finite products, that \([\mathscr{B}, \mathscr{C}]\) is again small and so is an object of \(\mathbf{Cat}\), and that the currying isomorphism already proved for functor categories is an adjunction.

The product category \(\mathscr{A} \times \mathscr{B}\), equipped with the two coordinate projections, is a product in \(\mathbf{Cat}\). Its objects, maps, composition and identities are all formed coordinatewise, so a functor \(\mathscr{X} \to \mathscr{A} \times \mathscr{B}\) is precisely a pair of functors \(\mathscr{X} \to \mathscr{A}\) and \(\mathscr{X} \to \mathscr{B}\), which is the universal property. The category \(\mathbf{1}\) with a single object and only its identity map is terminal, every functor into it being forced.

Smallness of \([\mathscr{B}, \mathscr{C}]\) follows from the argument that made \(\mathbf{Cat}\) locally small. A functor between small categories is set-sized data, so the functors \(\mathscr{B} \to \mathscr{C}\) form a set. A natural transformation between two of them is a family of maps of \(\mathscr{C}\) indexed by the objects of \(\mathscr{B}\), and both indexing collection and value collection are sets, so the natural transformations form a set as well. Hence \([\mathscr{B}, \mathscr{C}]\) is small.

Currying for functor categories supplies the adjunction. For small \(\mathscr{A}\), \(\mathscr{B}\) and \(\mathscr{C}\) it gives an isomorphism of categories \([\mathscr{A} \times \mathscr{B}, \mathscr{C}] \cong [\mathscr{A}, [\mathscr{B}, \mathscr{C}]]\), sending a functor \(D\) to \(\widehat{D}\) with \(\widehat{D}(A) = D(A, -)\) on objects and \(\widehat{D}(u) = D(u, -)\) on maps. Reading off the objects on the two sides is a bijection \[ \mathbf{Cat}\big(\mathscr{A} \times \mathscr{B}, \mathscr{C}\big) \cong \mathbf{Cat}\big(\mathscr{A}, [\mathscr{B}, \mathscr{C}]\big) . \]

What the definition demands beyond the bijection is naturality in \(\mathscr{A}\) and \(\mathscr{C}\), and the explicit formula for \(\widehat{D}\) supplies both. For a functor \(K : \mathscr{A}' \to \mathscr{A}\) the two functors \(\widehat{D \circ (K \times 1_{\mathscr{B}})}\) and \(\widehat{D} \circ K\) send an object \(A'\) of \(\mathscr{A}'\) to \(D(KA', -)\) and a map \(u\) of \(\mathscr{A}'\) to \(D(Ku, -)\), so they agree.

For a functor \(L : \mathscr{C} \to \mathscr{C}'\) the candidate right adjoint acts by postcomposition, \(L_* = [\mathscr{B}, L]\), and both \(\widehat{L \circ D}\) and \(L_* \circ \widehat{D}\) send \(A\) to \(L \circ D(A, -)\) and \(u\) to \(L \circ D(u, -)\). The bijection is therefore natural in both variables, and \(- \times \mathscr{B} \dashv [\mathscr{B}, -]\) on \(\mathbf{Cat}\).

Examples that fit tell little about the reach of a definition. The instructive question is which familiar categories fail to be cartesian closed, and what the failure costs them.

When Closure Fails

The two examples so far might suggest that any category whose maps assemble into an object of the same kind is cartesian closed. Vector spaces are the standard warning. Over a field \(k\), the linear maps \(V \to W\) form a vector space under pointwise addition and scaling, so \(\mathbf{Vect}_k\) has spaces of maps in the most literal sense available, and it is still not cartesian closed. The space of linear maps is a perfectly good object. It is simply adjoint to the wrong operation.

The direct sum defeats closure

Finite products are present. The direct sum \(V \oplus W\) with its two coordinate projections is a product in \(\mathbf{Vect}_k\), since a linear map \(U \to V \oplus W\) is exactly a pair of linear maps \(U \to V\) and \(U \to W\), read off coordinatewise. The zero space \(\{0\}\) is terminal and initial at once, the zero map being the only linear map into it and the only one out of it.

Suppose \(\mathbf{Vect}_k\) were cartesian closed and fix an object \(B\). Then \(- \times B\) has a right adjoint, and \(\mathbf{Vect}_k\) is locally small, the linear maps between two vector spaces forming a set, so left adjoints preserve colimits applies to it. An initial object is the colimit of the empty diagram, so preservation forces \(\{0\} \times B\) to be initial in \(\mathbf{Vect}_k\). The product is the direct sum, and \[ \{0\} \oplus B \cong B , \] the isomorphism sending \((0, b)\) to \(b\).

So \(B\) would be initial, and since initial objects are unique up to isomorphism, every object \(B\) whatsoever would be isomorphic to \(\{0\}\). The field \(k\) is itself a vector space over \(k\) and is not the zero space, a field having \(1 \neq 0\). The supposition fails, and \(\mathbf{Vect}_k\) is not cartesian closed.

The isomorphism \(0 \times B \cong 0\) in \(\mathbf{Set}\) is the statement just refuted, transported to another category. It was obtained from the currying adjunction as the categorical form of the annihilation of zero. Cartesian closure casts an arithmetic shadow, and the shadow is one that \(\mathbf{Vect}_k\) declines to cast, because its initial object is also its terminal object and a product with a terminal object absorbs nothing.

Bilinearity, and the operation that fits

The reason \([V, W]\), the space of linear maps from \(V\) to \(W\), fails to be an exponential is worth isolating, because the failure is precise rather than accidental.

A linear map \(\varphi : U \to [V, W]\) is the same data as a function \(b : U \times V \to W\) with \(b(u, v) = \varphi(u)(v)\). Linearity of \(\varphi\) makes \(b\) linear in its first argument, and linearity of each value \(\varphi(u)\) makes it linear in the second. Maps into \([V, W]\) therefore correspond to bilinear maps out of \(U \times V\). Linear maps \(U \oplus V \to W\) are pairs of linear maps, since such a map is determined by its restrictions to the two summands and any pair of linear maps on the summands arises from one. That is a different correspondence altogether.

The adjunction pattern survives once the operation on the left is changed to fit. The tensor product \(U \otimes V\) is the vector space whose defining property is exactly the one now wanted. Linear maps \(U \otimes V \to W\) correspond to bilinear maps \(U \times V \to W\). Its construction is not carried out here. Composing the two correspondences gives \[ \mathbf{Vect}_k\big(U \otimes V, W\big) \cong \mathbf{Vect}_k\big(U, [V, W]\big) , \] natural in \(U\) and in \(W\), since both correspondences are given by composition. A category carrying an adjunction of this shape for an operation that need not be the categorical product is called monoidal closed, and cartesian closure is the case where the operation is the product.

The distinction is not bookkeeping. The tensor product is not the categorical product in \(\mathbf{Vect}_k\), the direct sum already being that, and in finite dimensions the two are told apart by a dimension count, one multiplying where the other adds.

So \(U \otimes V\) arrives with no projections and no diagonal handed to it by a universal property, and a map out of a tensor product cannot in general read its two inputs separately, copy one of them, or throw one away. Compositional accounts of learning systems, in which a parameter is consumed by the process it feeds rather than duplicated across it, are naturally staged in monoidal closed rather than cartesian closed categories. The difference between the two is the difference this section has just measured.

Sets and small categories are closed, vector spaces are not. The category the rest of the page is about lies between the two in difficulty. Presheaf categories are cartesian closed, but their exponentials are not computed pointwise, and locating them takes nearly everything the surrounding pages have built.

Exponentials in a Presheaf Category

Throughout this section \(\mathbf{A}\) is a small category and presheaves on it are written \(X\), \(Y\), \(Z\).

Convention. The presheaf category \([\mathbf{A}^{\mathrm{op}}, \mathbf{Set}]\) is abbreviated \(\hat{\mathbf{A}}\) for the remainder of the page, since its hom-sets are displayed repeatedly in the argument ahead and the unabbreviated name would not fit on a line. It is locally small, a map of presheaves being a family of functions indexed by the objects of \(\mathbf{A}\) and so an element of a set-indexed product of sets.

Half of cartesian closure is already in hand. Presheaf categories are complete and cocomplete, so finite products exist, and the same result records that each evaluation functor preserves them, so that products of presheaves are computed pointwise. What is missing is the exponential, and the first thing to establish is that it cannot also be pointwise.

What the exponential is forced to be

When \(\mathbf{A}\) is discrete a presheaf is nothing but a family of sets indexed by the objects, a map of presheaves is a family of functions, and everything in sight is computed coordinate by coordinate. Cartesian closure is then inherited from \(\mathbf{Set}\) coordinatewise, exponentials included. The general case is not like this, and the quickest way to see what it must look like instead is to assume the conclusion and read off the consequence.

Suppose then that \(\hat{\mathbf{A}}\) were cartesian closed, with exponentials \(Z^Y\). Evaluating a presheaf at an object is the same as probing it by a representable, so for every \(A \in \mathbf{A}\) the Yoneda lemma followed by the adjointness bijection would give \[ Z^Y(A) \cong \hat{\mathbf{A}}\big(H_A, Z^Y\big) \cong \hat{\mathbf{A}}\big(H_A \times Y, Z\big) . \] The exponential is thereby forced. Its value at \(A\) has to be the set of maps \(H_A \times Y \to Z\).

Notice what that value is not. It is not \(Z(A)^{Y(A)}\), and exponentials in a presheaf category are accordingly not generally computed pointwise, in contrast with the products and colimits of the pages leading here. The value at \(A\) sees not only \(A\) but everything that maps into it.

Turn the consequence into a definition. Given presheaves \(Y\) and \(Z\), let \[ Z^Y(A) = \hat{\mathbf{A}}\big(H_A \times Y, Z\big) \] for each object \(A\), and for a map \(f : A' \to A\) of \(\mathbf{A}\) let \(Z^Y(f)\) send \(\sigma : H_A \times Y \to Z\) to \(\sigma \circ (H_f \times 1_Y) : H_{A'} \times Y \to Z\), where \(H_f : H_{A'} \to H_A\) is the image of \(f\) under the Yoneda embedding. Because \(H_\bullet\) is a functor and composition is associative, this assignment respects identities and composites in the direction required of a presheaf, so \(Z^Y\) is an object of \(\hat{\mathbf{A}}\).

Evaluation, and the map to be inverted

A candidate exponential is not an exponential until a bijection is produced, and a bijection produced one object at a time would not be enough. Adjointness demands naturality in \(X\) and in \(Z\), and naturality is a property of a map, not of a family of bijections. So the map comes first. In a cartesian closed category the map is composition with the counit, and here the counit can be written down.

Define \(\operatorname{ev} : Z^Y \times Y \to Z\) by \[ \operatorname{ev}_A(\sigma, y) = \sigma_A(1_A, y) \] for \(A \in \mathbf{A}\), \(\sigma \in Z^Y(A)\) and \(y \in Y(A)\), the product being pointwise. This is the only reasonable thing to write. An element of \(Z^Y(A)\) is a map \(H_A \times Y \to Z\) and the one element of \(H_A(A)\) that is always available is the identity.

Evaluation is natural. Let \(f : A' \to A\) in \(\mathbf{A}\). The presheaf \(Z^Y \times Y\) carries \((\sigma, y)\) to \(\big(\sigma \circ (H_f \times 1_Y), (Yf)(y)\big)\), and \[ \begin{align*} \operatorname{ev}_{A'}\big(\sigma \circ (H_f \times 1_Y), (Yf)(y)\big) &= \sigma_{A'}\big(H_f(1_{A'}), (Yf)(y)\big) \\\\ &= \sigma_{A'}\big(f, (Yf)(y)\big) \\\\ &= (Zf)\big(\sigma_A(1_A, y)\big) \\\\ &= (Zf)\big(\operatorname{ev}_A(\sigma, y)\big) , \end{align*} \] the second line because \(H_f\) sends \(1_{A'}\) to \(f \circ 1_{A'}\), and the third by the naturality of \(\sigma : H_A \times Y \to Z\) at \(f\), applied to the element \((1_A, y)\), whose image under \(H_A(f) \times Y(f)\) is \((1_A \circ f, (Yf)(y))\).

With evaluation in place, define for every presheaf \(X\) \[ \Theta_X : \hat{\mathbf{A}}\big(X, Z^Y\big) \to \hat{\mathbf{A}}\big(X \times Y, Z\big), \quad \Theta_X(\varphi) = \operatorname{ev} \circ (\varphi \times 1_Y) , \] whose value on components reads \(\Theta_X(\varphi)_A(x, y) = \big(\varphi_A(x)\big)_A(1_A, y)\).

Three properties come for nothing. The values of \(\Theta_X\) are maps of presheaves, being composites of such maps. It is natural in \(X\), since precomposing \(\varphi\) with \(k : X' \to X\) precomposes \(\Theta_X(\varphi)\) with \(k \times 1_Y\). And it is natural in \(Z\). For \(t : Z \to Z'\), postcomposition with \(t\) is a map of presheaves \(t_* : Z^Y \to (Z')^Y\), by associativity of composition, and it makes \(Z \mapsto Z^Y\) a functor, identities and composites being preserved for the same reason. Naturality reduces to the identity \(\operatorname{ev}' \circ (t_* \times 1_Y) = t \circ \operatorname{ev}\), since precomposing it with \(\varphi \times 1_Y\) turns \(\operatorname{ev}' \circ \big((t_* \circ \varphi) \times 1_Y\big)\) into \(t \circ \Theta_X(\varphi)\), and both of its sides send \((\sigma, y)\) to \(t_A(\sigma_A(1_A, y))\).

Everything therefore rests on a single question, and it is a question about one map rather than about a family of sets: is \(\Theta_X\) a bijection?

Two tools

The first tool is the dual of the fact that representables preserve limits. Applied in \(\mathscr{S}^{\mathrm{op}}\), which is locally small exactly when \(\mathscr{S}\) is, that proposition concerns the covariant hom-functor of the opposite category based at an object \(W\), which is the contravariant hom-functor \(\mathscr{S}(-, W)\). A colimit cocone on a diagram \(D\) is a limit cone on \(D^{\mathrm{op}}\). The dualization was recorded when the proposition was proved, there in isomorphism form.

In cone form the statement reads as follows. If \(\big(D(I) \to C\big)_{I \in \mathbf{I}}\) is a colimit cocone in a locally small \(\mathscr{S}\), then \[ \Big(\mathscr{S}(C, W) \to \mathscr{S}\big(D(I), W\big)\Big)_{I \in \mathbf{I}^{\mathrm{op}}}, \] with legs given by precomposition with the coprojections, is a limit cone in \(\mathbf{Set}\). Colimits go in, limits come out.

The second tool converts cartesian closure of \(\mathbf{Set}\) into a statement about presheaves. Closure is not a curiosity about sets. It propagates.

The proof is worth reading twice for its shape rather than its content. The currying adjunction on \(\mathbf{Set}\), the single concrete adjunction these pages began with, is fed to the preservation theorem, and what comes out is a statement about presheaves on an arbitrary small category. The bootstrap is the whole mechanism.

The exponential exists

Read backwards, the proof is an inventory of the surrounding pages. Yoneda supplies the representable case, density reduces the general case to it, representables preserving limits converts colimits of presheaves into limits of hom-sets, and the preservation theorem for adjoints, applied to currying in \(\mathbf{Set}\), supplies the one step where the two variables interact. The exponential of presheaves is not built by hand. It is assembled out of results that were proved for other reasons.

Function Types and the Logic of Presheaves

A definition earns its keep by what it turns out to be equivalent to. Cartesian closure has two such second lives, one in the theory of programming languages and one in the theory of toposes, and the exponential just constructed sits at the junction.

Types

The correspondence between logic and type theory lines up propositions with types: a conjunction with a product type, a disjunction with a sum type, an implication with a function type, truth with the unit type and falsity with the empty type.

Read that dictionary once more with a cartesian closed category in view and a third column appears. A product type is a product, a function type \(B \to C\) is an exponential \(C^B\), and the unit type is the terminal object. The transposition that carries a map \(A \times B \to C\) to a map \(A \to C^B\) is the operation a programmer knows as currying and a logician as the deduction theorem. Evaluation \(\operatorname{ev} : C^B \times B \to C\) is function application.

Several rows of the dictionary reach past cartesian closure and it is worth saying where the boundary lies. Sum types and the empty type ask for coproducts and an initial object, which a cartesian closed category is not required to have. The dependent function and pair types ask for more still, a compatibility of exponentials with slicing that the present definition does not mention.

What the theorem of the previous section delivers is the simply typed fragment, and it delivers it exactly. The syntactic category built from a simply typed calculus is cartesian closed, and every cartesian closed category interprets that calculus, the two passages being mutually inverse up to the appropriate notion of sameness. That equivalence, due to Joachim Lambek, is a substantial theorem, and it is not proved here. What is proved here is that presheaf categories are on the semantic side of it.

Toposes

The other second life begins from an observation about \(\mathbf{Set}\) already on record. Subsets of a set \(A\) correspond to functions \(A \to 2\), so that the power set is the exponential \(2^A\), and the two-element set does for subsets what an exponential does for maps. That set turns a property into an object of the category. An object with this behaviour is called a subobject classifier. Its formal definition requires the notion of subobject, which this page does not develop, and the discussion here goes no further than naming the pattern.

A topos is a cartesian closed category with finite limits and a subobject classifier. Of the three requirements, presheaf categories have now been shown to meet the first, and they meet the second with room to spare, having all limits and not merely the finite ones. They meet the third as well, though stating the classifier explicitly would call for the definition just deferred. Taking \(\mathbf{A}\) to be the terminal category recovers \(\mathbf{Set}\). So cartesian closure, the part established above, is the hard third of the statement that every presheaf category is a topos.

The name carries two readings that pull in opposite directions and are both accurate. A topos is a universe of sets, in which one may reason about objects as though they were sets, with the caution that the reasoning permitted is intuitionistic rather than classical. A topos is also a generalized space, of which the presheaf categories are the tamest examples, and the topological properties of a space can be read off from categorical properties of an associated topos. Neither reading is developed further here.

The arc of these pages closes on itself. It opened by asking what a functor with an adjoint does to limits, and the answer, that a right adjoint preserves them, looked at the time like a technical convenience. That convenience was the engine. Applied to the diagonal it explained why limits commute with limits. Applied to currying in \(\mathbf{Set}\), and combined with density and the Yoneda lemma, it produced an exponential in a category no one constructed by hand. With that exponential came a universe in which sets, spaces, and the terms of a typed calculus are all describable as the same kind of object.