nLab cartesian closed category



Monoidal categories

monoidal categories

With braiding

With duals for objects

With duals for morphisms

With traces

Closed structure

Special sorts of products



Internal monoids



In higher category theory

Category theory



A cartesian closed category (sometimes: ccc) is a category with finite products which is closed with respect to its cartesian monoidal structure.

The internal hom [S,X][S,X] in a cartesian closed category is often called exponentiation and is denoted X SX^S.

A cartesian closed functor between cartesian closed categories CC, DD is a functor F:CDF \colon C \to D that is product-preserving and that is also exponential-preserving, meaning that the canonical map

F(a b)F(a) F(b),F(a^b) \to F(a)^{F(b)},

corresponding to the composite

F(a b)×F(b)F(a b×b)F(eval a,b)F(a),F(a^b) \times F(b) \cong F(a^b \times b) \stackrel{F(eval_{a, b})}{\to} F(a),

is an isomorphism.


Some basic consequences

A category is cartesian closed if it has finite products and if for any two objects XX, YY, there is an object Y XY^X (thought of as a “space of maps from XX to YY”) such that for any object ZZ, there is a bijection between the set of maps ZY XZ \to Y^X and the set of maps Z×XYZ \times X \to Y, and this bijection is natural in ZZ.

There is an evaluation map ev X,Y:Y X×XYev_{X, Y}: Y^X \times X \to Y, which by definition is the map corresponding to the identity map Y XY XY^X \to Y^X under the bijection. Using the naturality, it may be shown that the bijection hom(Z,Y X)hom(Z×X,Y)\hom(Z, Y^X) \to \hom(Z \times X, Y) takes a map ϕ:ZY X\phi: Z \to Y^X to the composite

Z×Xϕ×1 XY X×Xev X,YYZ \times X \stackrel{\phi \times 1_X}{\to} Y^X \times X \stackrel{ev_{X, Y}}{\to} Y

and the universal property of Y XY^X may be phrased thus: given any ψ:Z×XY\psi: Z \times X \to Y, there exists a unique map ϕ:ZY X\phi: Z \to Y^X for which ψ=ev X,Y(ϕ×1 X)\psi = ev_{X, Y} \circ (\phi \times 1_X).

Taking Z=1Z = 1 (the terminal object), maps 1Y X1 \to Y^X (or “points” of Y XY^X) are in bijection with maps Xπ 2 11×XYX \stackrel{\pi_{2}^{-1}}{\to} 1 \times X \to Y. So the “underlying set” of Y XY^X, namely hom(1,Y X)\hom(1, Y^X), is identified with the set of maps from XX to YY. Let us denote the point corresponding to f:XYf: X \to Y by [f]:1Y X[f]: 1 \to Y^X. Then, by definition,

(1×X[f]×1 XY X×Xev X,YY)=(1×Xπ 2XfY)(1 \times X \stackrel{[f] \times 1_X}{\to} Y^X \times X \stackrel{ev_{X, Y}}{\to} Y) = (1 \times X \stackrel{\pi_2}{\to} X \stackrel{f}{\to} Y)

The following lemma says that the internal evaluation map ev X,Yev_{X, Y} indeed behaves as an evaluation map at the level of underlying sets.


Given a map f:XYf: X \to Y and a point x:1Xx: 1 \to X, the composite

1[f],xY X×Xev X,YY1 \stackrel{\langle [f], x \rangle}{\to} Y^X \times X \stackrel{ev_{X, Y}}{\to} Y

is the point fx:1Yf x: 1 \to Y.


We have

1[f],xY X×Xev X,YX = 1δ 11×1[f]×xY X×Xev X,YY = 1δ 11×11×x1×X[f]×1 XY X×Xev X,YY = 1δ 11×11×x1×Xπ 2XfY = 1δ 11×1π 21xXfY = 1xXfY\array{ 1 \stackrel{\langle [f], x \rangle}{\to} Y^X \times X \stackrel{ev_{X, Y}}{\to} X & = & 1 \stackrel{\delta_1}{\to} 1 \times 1 \stackrel{[f] \times x}{\to} Y^X \times X \stackrel{ev_{X, Y}}{\to} Y\\ & = & 1 \stackrel{\delta_1}{\to} 1 \times 1 \stackrel{1 \times x}{\to} 1 \times X \stackrel{[f] \times 1_X}{\to} Y^X \times X \stackrel{ev_{X, Y}}{\to} Y\\ & = & 1 \stackrel{\delta_1}{\to} 1 \times 1 \stackrel{1 \times x}{\to} 1 \times X \stackrel{\pi_2}{\to} X \stackrel{f}{\to} Y\\ & = & 1 \stackrel{\delta_1}{\to} 1 \times 1 \stackrel{\pi_2}{\to} 1 \stackrel{x}{\to} X \stackrel{f}{\to} Y\\ & = & 1 \stackrel{x}{\to} X \stackrel{f}{\to} Y }

where the penultimate equation uses naturality of the projection map π 2\pi_2.


Internal composition c X,Y,Z:Z Y×Y XZ Xc_{X, Y, Z}: Z^Y \times Y^X \to Z^X is the unique map such that

(Z Y×Y X×Xc×1 XZ X×Xev X,ZZ)=(Z Y×Y X×X1×ev X,YZ Y×Yev Y,ZZ)(Z^Y \times Y^X \times X \stackrel{c \times 1_X}{\to} Z^X \times X \stackrel{ev_{X, Z}}{\to} Z) = (Z^Y \times Y^X \times X \stackrel{1 \times ev_{X, Y}}{\to} Z^Y \times Y \stackrel{ev_{Y, Z}}{\to} Z)

One may show that internal composition behaves as the usual composition at the underlying set level, in that given maps g:YZg: Y \to Z, f:XYf: X \to Y, we have

(1[g],[f]Z Y×Y Xc X,Y,ZZ X)=[gf]:1Z X(1 \stackrel{\langle [g], [f] \rangle}{\to} Z^Y \times Y^X \stackrel{c_{X, Y, Z}}{\to} Z^X) = [g f]: 1 \to Z^X


Inheritance by reflective subcategories

In showing that a given category is cartesian closed, the following theorem is often useful (cf. A4.3.1 in the Elephant):


If CC is cartesian closed, and DCD\subseteq C is a reflective subcategory, then the reflector L:CDL\colon C\to D preserves finite products if and only if DD is an exponential ideal (i.e. YDY\in D implies Y XDY^X\in D for any XCX\in C). In particular, if LL preserves finite products, then DD is cartesian closed.

Exponentials of cartesian closed categories

The following observation was taken from a post of Mike Shulman at MathOverflow.

If 𝒞\mathcal{C} is small and 𝒟\mathcal{D} is complete and cartesian closed, then 𝒟 𝒞\mathcal{D}^{\mathcal{C}} is also complete and cartesian closed. Completeness is clear since limits in D CD^C are computed pointwise. As for cartesian closure, we can compute exponentials in essentially the same way as for presheaves, motivated by 𝒟\mathcal{D}-enriched category theory:

G F(x)= y𝒞 𝒞(x,y)G(y) F(y). G^F(x) = \int_{y\in \mathcal{C}} \prod_{\mathcal{C}(x,y)} G(y)^{F(y)}.

Then we can compute

𝒟 𝒞(H,G F) = x𝒞𝒟(H(x),G F(x)) = x𝒞𝒟(H(x), y𝒞 𝒞(x,y)G(y) F(y)) = x𝒞 y𝒞 𝒞(x,y)𝒟(H(x),G(y) F(y)) = y𝒞𝒟( x𝒞 𝒞(x,y)H(x),G(y) F(y)) = y𝒞𝒟(H(y),G(y) F(y)) = y𝒞𝒟(H(y)×F(y),G(y)) = 𝒟 𝒞(H×F,G).\array{ \mathcal{D}^{\mathcal{C}}\left(H,G^F\right) &=& \int_{x\in \mathcal{C}} \mathcal{D}\left(H(x), G^F(x)\right)\\ &=& \int_{x\in \mathcal{C}} \mathcal{D}\left(H(x), \int_{y\in \mathcal{C}} \prod_{\mathcal{C}(x,y)} G(y)^{F(y)}\right)\\ &=& \int_{x\in \mathcal{C}} \int_{y\in \mathcal{C}} \prod_{\mathcal{C}(x,y)} \mathcal{D}\left(H(x), G(y)^{F(y)}\right)\\ &=& \int_{y\in \mathcal{C}} \mathcal{D}\left( \int^{x\in \mathcal{C}} \sum_{\mathcal{C}(x,y)} H(x), G(y)^{F(y)}\right)\\ &=& \int_{y\in \mathcal{C}} \mathcal{D}\left(H(y), G(y)^{F(y)}\right)\\ &=& \int_{y\in \mathcal{C}} \mathcal{D}\left(H(y)\times F(y), G(y)\right)\\ &=& \mathcal{D}^{\mathcal{C}}(H\times F, G). }

Here the antepenultimate step uses the co-Yoneda lemma. This appears to involve colimits in 𝒟\mathcal{D} as well, but the existence of these colimits is not actually an extra assumption: the co-Yoneda lemma tells us that x𝒞 𝒞(x,y)H(x)\int^{x\in \mathcal{C}} \sum_{\mathcal{C}(x,y)} H(x) exists and is isomorphic to H(y)H(y).

Similarly, the above argument can be interpreted to say that even if 𝒟\mathcal{D} is not complete, then the exponential G FG^F in 𝒟 𝒞\mathcal{D}^{\mathcal{C}} exists if and only if the particular limits above exist, and in that case they are isomorphic.

A more abstract argument using comonadicity and the adjoint triangle theorem, which also applies to locally cartesian closed categories, can be found in Theorem 2.12 of

  • Street and Verity, The comprehensive factorization and torsors, TAC

and is reproduced in the setting of closed monoidal categories at closed monoidal category.

Functional completeness theorem


Let CC be a cartesian closed category, and cc an object of CC. Then the Kleisli category of the comonad c×:CCc \times - \colon C \to C, denoted C[c]C[c], is also a cartesian closed category.


The Kleisli category of the comonad c×c \times - on CC is canonically equivalent to the Kleisli category of the monad () c(-)^c on CC.


of Theorem

Let aa and bb be objects of C[c]C[c]. Claim: the product a×ba \times b in CC, considered as an object of C[c]C[c], is the product of aa and bb in C[c]C[c], according to the following series of natural bijections:

zazb̲ C[c] c×za,c×zb̲ C c×za×b̲ C za×b C[c]\array{ \underline{z \to a \qquad z \to b} & C[c] \\ \underline{c \times z \to a, c \times z \to b} & C \\ \underline{c \times z \to a \times b} & C \\ z \to a \times b & C[c] }

Claim: the exponential a ba^b in CC, considered as an object of C[c]C[c], is the exponential of aa and bb in C[c]C[c], according to the following series of natural bijections:

za b̲ C[c] c×za b̲ C c×z×ba̲ C z×ba C[c]\array{ \underline{z \to a^b} & C[c] \\ \underline{c \times z \to a^b} & C \\ \underline{c \times z \times b \to a} & C \\ z \times b \to a & C[c] }

where in the last step, we used the prior claim that the product of objects in CC, when viewed as an object of C[c]C[c], gives the product in C[c]C[c].

Observe that the object cc in C[c]C[c] has an element e:1ce \colon 1 \to c, corresponding to the canonical isomorphism c×1cc \times 1 \cong c in CC. We call this element the “generic element” of cc in C[c]C[c], according to the following theorem. This theorem can be viewed as saying that in the doctrine of cartesian closed categories, C[c]C[c] is the result of freely adjoining an arrow 1c1\to c to CC.


(Functional completeness)

Let CC and DD be cartesian closed categories, and let F:CDF \colon C \to D be a cartesian closed functor. Let cc be an object of CC, and let t:F(1)F(c)t: F(1) \to F(c) be an element in DD. Then there exists an extension of FF to a cartesian closed functor F˜:C[c]D\tilde{F} \colon C[c] \to D that takes the generic element e:1ce \colon 1 \to c in C[c]C[c] to the element tt, and this extension is unique up to isomorphism.

Proof (sketch)

On objects, F˜(a)=F(a)\tilde{F}(a) = F(a). Let f:abf \colon a \to b be a map of C[c]C[c], i.e., let g:c×abg \colon c \times a \to b be the corresponding map in CC, and define F˜(f)\tilde{F}(f) to be the composite

F(a)1×F(a)t×1F(c)×F(a)F(c×a)F(g)F(b)F(a) \cong 1 \times F(a) \stackrel{t \times 1}{\to} F(c) \times F(a) \cong F(c \times a) \stackrel{F(g)}{\to} F(b)

It is straightforward to check that F˜\tilde{F} is a cartesian closed functor and is, up to isomorphism, the unique cartesian closed functor taking ee to tt.


Textbook accounts:

Discussion with focus on mapping spaces (compact-open topology) in topological spaces and compactly generated topological spaces:

See also the references at exponential object.

Establishing the syntax/semantics relation between cartesian closed categories and simply-typed lambda calculi:

A proof that a cartesian closed category is posetal if it satisfies an equality of morphisms not satisfied in a free cartesian closed category:

  • Kosta Dosen, and Zoran Petric. The maximality of the typed lambda calculus and of cartesian closed categories (1999), (arXiv:math/9911073)

Last revised on October 7, 2023 at 21:48:53. See the history of this page for a list of all contributions to it.