locally cartesian closed category


Category Theory

Monoidal categories

monoidal categories

With symmetry

With duals for objects

With duals for morphisms

With traces

Closed structure

Special sorts of products



Internal monoids



In higher category theory



A locally cartesian closed category is a category CC whose slice categories C/xC/x are all cartesian closed.

If a locally cartesian closed category CC has a terminal object, then CC is itself cartesian closed and in fact has all finite limits (because, cartesian products in C/xC/x are pullbacks in CC); often this requirement is included in the definition.

Equivalently, a locally cartesian closed category CC is a category with pullbacks (and a terminal object, if required) such that each base change functor f *:C/y→C/xf^*: C/y \to C/x has a right adjoint Π f\Pi_f, called the dependent product. (This equivalence is discussed in detail below.)

In particular, such pullbacks preserve all colimits. Therefore, if a locally cartesian closed category has finite colimits, it is automatically a coherent category and in fact a Heyting category.


Cartesian closure in terms of base change and dependent product

We show how the dependent product and the internal hom in the slice categories may be used to express each other.

In category theory


Let π’ž\mathcal{C} be a category with pullbacks that has all dependent products ∏ β€’\prod_\bullet, equivalently that every morphism f:Eβ†’Xf : E \to X in π’ž\mathcal{C} induces an adjoint triple

π’ž /E⟢∏ f⟡f *βŸΆβˆ‘ fπ’ž /X. \mathcal{C}_{/E} \stackrel{\overset{\sum_f}{\longrightarrow}}{\stackrel{\overset{f^*}{\longleftarrow}}{\underset{\prod_f}{\longrightarrow}}} \mathcal{C}_{/X} \,.

Then the internal hom in a slice π’ž /X\mathcal{C}_{/X} exists and is given by

[⟨E⟢fX⟩,βˆ’] π’ž /Xβ‰ƒβˆ f∘f *. [\langle E \stackrel{f}{\longrightarrow} X\rangle \; ,\; -]_{\mathcal{C}_{/X}} \simeq \prod_f \circ f^* \,.

By the discussion at overcategory-Limits and colimits the product in the slice π’ž /X\mathcal{C}_{/X} of two objects ⟨E 1⟢f 1X⟩\langle E_1 \stackrel{f_1}{\longrightarrow} X\rangle and ⟨E 2⟢f 2X⟩\langle E_2 \stackrel{f_2}{\longrightarrow} X\rangle is given by the pullback f 1 *E 2=f 2 *E 1f_1^* E_2 = f_2^* E_1 in π’ž\mathcal{C}, regarded again as a morphism over XX. More formally this means that the product with ⟨Eβ†’fX⟩\langle E \stackrel{f}{\to} X\rangle is given by the composite

(βˆ’)Γ— π’ž /X⟨Eβ†’fX⟩:π’ž /Xβ†’f *π’ž /Eβ†’βˆ‘ fπ’ž /X (-) \times_{\mathcal{C}_{/X}} \langle E \stackrel{f}{\to} X\rangle \;\;\;:\;\;\; \mathcal{C}_{/X} \stackrel{f^*}{\to} \mathcal{C}_{/E} \stackrel{\sum_f}{\to} \mathcal{C}_{/X}

of the pullback along ff with the dependent sum along ff. By the above adjoint triple both these morphisms have right adjoints and so the composite of the right adjoints is the right adjoint of the composite, hence is the internal hom:

π’ž /Xβ†βˆ fπ’ž /E←f *π’ž /X:[⟨Eβ†’fX⟩,βˆ’] π’ž /X. \mathcal{C}_{/X} \stackrel{\prod_f}{\leftarrow} \mathcal{C}_{/E} \stackrel{f^* }{\leftarrow} \mathcal{C}_{/X} \;\;\;:\;\;\; [\langle E\stackrel{f}{\to} X \rangle, -]_{\mathcal{C}_{/X}} \,.

In the slice category Set/XSet/X, the inner hom is explicitly given by

[⟨Eβ†’fX⟩,⟨Fβ†’gX⟩] Set/X={(x,h)|x∈X,h:f βˆ’1(x)β†’g βˆ’1(x)}. [\langle E \stackrel{f}{\to} X \rangle, \langle F \stackrel{g}{\to} X \rangle]_{Set/X} = \{ (x,h) | x \in X, h : f^{-1}(x) \to g^{-1}(x) \}.

If for a category π’ž\mathcal{C} every slice category is a cartesian closed category, then for every morphism f:Xβ†’Yf : X \to Y in π’ž\mathcal{C} the dependent product ∏ f\prod_f exists and is given on an object Eβ†’pXE \stackrel{p}{\to} X by the pullback

∏ f⟨Eβ†’pX⟩ β†’ [⟨Xβ†’fY⟩,⟨Eβ†’pXβ†’fY⟩] π’ž /Y ↓ ↓ Y β†’idΒ― [⟨Xβ†’fY⟩,⟨Xβ†’fY⟩] π’ž /Y \array{ \prod_f \langle E \stackrel{p}{\to} X\rangle &\to& [\langle X \stackrel{f}{\to}Y\rangle, \langle E \stackrel{p}{\to}X \stackrel{f}{\to} Y\rangle]_{\mathcal{C}_{/Y}} \\ \downarrow && \downarrow \\ Y &\stackrel{\bar id}{\to}& [\langle X \stackrel{f}{\to}Y \rangle,\langle X \stackrel{f}{\to}Y \rangle]_{\mathcal{C}_{/Y}} }

in π’ž /Y\mathcal{C}_{/Y}, where the bottom morphism is the adjunct of

YΓ— π’ž /Y⟨Xβ†’fYβŸ©β‰ƒβŸ¨Xβ†’fYβŸ©β†’id⟨Xβ†’fY⟩. Y \times_{\mathcal{C}_{/Y}} \langle X \stackrel{f}{\to} Y\rangle \simeq \langle X \stackrel{f}{\to}Y\rangle \stackrel{id}{\to} \langle X \stackrel{f}{\to}Y\rangle \,.

It is sufficient to check the (f *⊣∏ f)(f^* \dashv \prod_f)-adjunction hom set-natural isomorphism

π’ž /Y(⟨Fβ†’Y⟩,∏ f⟨Eβ†’pX⟩)β‰ƒπ’ž /X(f *⟨Fβ†’Y⟩,⟨Eβ†’pX⟩), \mathcal{C}_{/Y}( \langle F \stackrel{}{\to} Y\rangle , \prod_f \langle E \stackrel{p}{\to} X\rangle) \simeq \mathcal{C}_{/X}(f^* \langle F \stackrel{}{\to} Y\rangle, \langle E \stackrel{p}{\to} X\rangle) \,,

natural in ⟨Fβ†’Y⟩\langle F \stackrel{}{\to}Y \rangle.

Since the hom functor π’ž /Y(⟨Fβ†’Y⟩,βˆ’)\mathcal{C}_{/Y}(\langle F \stackrel{}{\to} Y\rangle, -) preserves limits and hence pullbacks, the expression on the left is exhibited as the pullback

π’ž /Y(⟨Fβ†’Y⟩,∏ f⟨Eβ†’pX⟩) β†’ π’ž /Y(⟨Fβ†’Y⟩,[⟨Xβ†’fY⟩,⟨Eβ†’pXβ†’fY⟩] π’ž /Y) ↓ ↓ * β†’ π’ž /Y(⟨Fβ†’Y⟩,[⟨Xβ†’fY⟩,⟨Xβ†’fY⟩] π’ž /Y) \array{ \mathcal{C}_{/Y}(\langle F \stackrel{}{\to} Y\rangle, \prod_f \langle E \stackrel{p}{\to} X\rangle) &\to& \mathcal{C}_{/Y}(\langle F \stackrel{}{\to} Y\rangle, [\langle X \stackrel{f}{\to}Y \rangle,\langle E \stackrel{p}{\to}X \stackrel{f}{\to} Y\rangle]_{\mathcal{C}_{/Y}}) \\ \downarrow && \downarrow \\ * &\stackrel{}{\to}& \mathcal{C}_{/Y}(\langle F \stackrel{}{\to} Y\rangle,[\langle X \stackrel{f}{\to}Y \rangle,\langle X \stackrel{f}{\to}Y \rangle]_{\mathcal{C}_{/Y}}) }

in Set. Using the ((βˆ’)Γ— π’ž /Y⟨Xβ†’fY⟩⊣[⟨Xβ†’fY⟩,βˆ’] π’ž /Y)((-) \times_{\mathcal{C}_{/Y}} \langle X \stackrel{f}{\to}Y\rangle \dashv [\langle X \stackrel{f}{\to}Y\rangle, -]_{\mathcal{C}_{/Y}})-adjunction this is equivalently

π’ž /Y(⟨Fβ†’Y⟩,∏ f⟨Eβ†’pX⟩) β†’ π’ž /Y(⟨Fβ†’YβŸ©Γ— π’ž /Y⟨Xβ†’fY⟩,⟨Eβ†’pXβ†’fY⟩) ↓ ↓ * β†’ π’ž /Y(⟨Fβ†’YβŸ©Γ— π’ž /Y⟨Xβ†’fY⟩,⟨Xβ†’fY⟩). \array{ \mathcal{C}_{/Y}(\langle F \stackrel{}{\to} Y\rangle, \prod_f \langle E \stackrel{p}{\to} X\rangle) &\to& \mathcal{C}_{/Y}(\langle F \stackrel{}{\to} Y\rangle \times_{\mathcal{C}_{/Y}} \langle X \stackrel{f}{\to}Y \rangle, \langle E \stackrel{p}{\to}X \stackrel{f}{\to} Y\rangle) \\ \downarrow && \downarrow \\ * &\stackrel{}{\to}& \mathcal{C}_{/Y}(\langle F \stackrel{}{\to} Y\rangle \times_{\mathcal{C}_{/Y} }\langle X \stackrel{f}{\to}Y \rangle , \langle X \stackrel{f}{\to}Y \rangle) } \,.

This pullback now manifestly computes π’ž /X(f *⟨Fβ†’Y⟩,⟨Eβ†’pX⟩)\mathcal{C}_{/X}(f^* \langle F \to Y\rangle, \langle E \stackrel{p}{\to} X\rangle).


If CC is locally cartesian closed (i.e., if every slice C/XC/X is cartesian closed), then every slice C/XC/X is also locally cartesian closed.


The slice of a slice is a slice, i.e., for every f:X→Yf \colon X \to Y there is an equivalence

(C/Y)/(f:Xβ†’Y)≃C/X(C/Y)/(f \colon X \to Y) \simeq C/X

whence the statement immediately follows.


If CC is locally cartesian closed (and has a terminal object), then the pullback functor XΓ—βˆ’:Cβ†’C/XX \times - \colon C \to C/X preserves both finite products and exponentials up to isomorphism.


Clearly XΓ—βˆ’:Cβ†’C/xX \times - \colon C \to C/x, being right adjoint to the forgetful functor βˆ‘ X:C/Xβ†’C\sum_X \colon C/X \to C, preserves limits, hence it preserves finite products in particular.

Let ϕ:A→X\phi \colon A \to X be any morphism. From the pullback diagram

AΓ—Z →ϕ×1 XΓ—Z Ο€ A↓ ↓ Ο€ X A β†’Ο• X\array{ A \times Z & \stackrel{\phi \times 1}{\to} & X \times Z \\ _\mathllap{\pi_A} \downarrow & & \downarrow _\mathrlap{\pi_X} \\ A & \underset{\phi}{\to} & X }

we conclude AΓ— X(XΓ—Z)β‰…AΓ—ZA \times_X (X \times Z) \cong A \times Z, seen as an object over XX via Ο•βˆ˜Ο€ A:AΓ—Zβ†’X\phi \circ \pi_A \colon A \times Z \to X. Thus arrows in the slice C/XC/X of the form

AΓ— X(XΓ—Z)β†’XΓ—YA \times_X (X \times Z) \to X \times Y

are in natural bijection with arrows in CC of the form

AΓ—Zβ†’βŸ¨Ο•βˆ˜Ο€ A,g⟩XΓ—YA \times Z \stackrel{\langle \phi \circ \pi_A, g\rangle}{\to} X \times Y

which in turn are in natural bijection with arrows in the slice C/XC/X of the form

Aβ†’βŸ¨Ο•,g˜⟩XΓ—Y ZA \stackrel{\langle \phi, \tilde{g} \rangle}{\to} X \times Y^Z

(where g˜:Aβ†’Y Z\tilde{g} \colon A \to Y^Z is obtained by currying g:AΓ—Zβ†’Yg \colon A \times Z \to Y in CC). This proves that XΓ—βˆ’:Cβ†’C/xX \times - \colon C \to C/x preserves exponentials.


For any f:Xβ†’Yf \colon X \to Y in CC, the base change f *:C/Yβ†’C/Xf^\ast \colon C/Y \to C/X preserves exponentials. In other words, the dependent sum functor βˆ‘ f\sum_f and the dependent product functor ∏ f\prod_f satisfy Frobenius reciprocity.


This is by combining proposition and proposition , and recalling that the pullback functor

C/Yβ†’(C/Y)/(f:Xβ†’Y)≃C/XC/Y \to (C/Y)/(f \colon X \to Y) \simeq C/X

is identified with the pullback functor f *:C/Y→C/Xf^\ast \colon C/Y \to C/X.

This state of affairs may be summarized in terms of the notion of hyperdoctrine:


If CC is a category with finite limits, then it is locally cartesian closed precisely if regarded as an CC-indexed category (by forming slice categories) it is a hyperdoctrine.

For a proof of the statement in this form, see for instance (Freyd).

In type theory

We formulate some of the above considerations in the syntax of dependent type theory.



X A Ο•β†˜ ↙ c B \array{ X &&&& A \\ & {}_{\mathllap{\phi}}\searrow && \swarrow_{\mathrlap{c}} \\ && B }

be two display maps. Then the category theoretic identification

[X,A] B=∏ ϕϕ *⟨Aβ†’cB⟩ [X,A]_{B} = \prod_\phi \phi^* \langle A \stackrel{c}{\to} B\rangle

from prop. is the categorical semantics of the dependent type theory syntax

b:B⊒X(b)β†’A(b):Type= defb:B⊒∏ x:X(b)A(Ο•(x)). b : B \vdash X(b) \to A(b) : Type \;\;\; =_{def} \;\;\; b : B \vdash \prod_{x : X(b)} A(\phi(x)) \,.

While equivalent under the relation between type theory and category theory, the latter expression almost verbatim expresses the evident idea that:

(collection of internal homs parameterized over BB) = ( collection of sections of the pullback of AA to XX )


By definition, the display map on the right is expressed as the dependent type

b:B⊒A(b):Type, b : B \vdash A(b) : Type \,,

the pullback Ο• *⟨Aβ†’B⟩\phi^* \langle A \to B\rangle is expressed by substitution

x:X⊒A(Ο•(x)):Type x : X \vdash A(\phi(x)) : Type

and next the dependent product ∏ ϕϕ *⟨Aβ†’B⟩\prod_\phi \phi^* \langle A \to B\rangle by

b:B⊒∏ x:X(b)A(Ο•(x)):Type. b : B \vdash \prod_{x : X(b)} A(\phi(x)) : Type \,.

Now on the right Ο•(x)= defb\phi(x) =_{def} b, formally because Ο•\phi is equivalently the projection pr 1pr_1 out of XX expressed as the direct sum

(b,x):βˆ‘ b:BX(b)pr 1(b,x)= defb= defΟ•(x):B. \frac{(b,x) : \sum_{b : B} X(b)} { pr_1(b,x) =_{def} b =_{def} \phi(x) : B} \,.

Inserting this in the above expression makes it definitionally equal to

b:B⊒∏ x:X(b)A(b):Type. b : B \vdash \prod_{x : X(b)} A(b) : Type \,.

This is now a dependent product over a type that does not actually depend on the context BB, and hence by definition this is the dependent function type

b:B⊒X(b)β†’A(b):Type. b : B \vdash X(b) \to A(b) : Type \,.

which expresses the internal hom in the slice over BB.

Internal logic

The internal logic of locally cartesian closed categories is an extensional form of dependent type theory. In particular, the dependent product Ξ  f\Pi_f represents an extensional dependent product type in the internal logic.

Almost local cartesian closure

There are categories which are cartesian closed and not locally cartesian closed, but in which for some ff the base change functor f *:C/y→C/xf^*: C/y \to C/x has a right adjoint. This includes CatCat, GpdGpd, and the category of crossed complexes; in the latter two cases, it is necessary and sufficient for ff to be a fibration, while in CatCat it is sufficient for ff to be a fibration or an opfibration.



Every sheaf topos is locally cartesian closed.


By Giraud's theorem, in a sheaf topos pullbacks preserve colimits. With the adjoint functor theorem this implies that for every morphism f:Xβ†’Yf : X \to Y, the pullback functor f *:π’ž /Yβ†’π’ž /Xf^* : \mathcal{C}_{/Y} \to \mathcal{C}_{/X} has a right adjoint ∏ f\prod_f. By prop. this yields the local cartesian closure.

More generally, every quasitopos is locally cartesian closed.


A standard textbook account is around corollary A1.5.3 in

The relation between local cartesian closure and base change/hyperdoctrine structure is sometimes attributed to

A discussion of dependent type theory as the internal language of locally cartesian closed categories is in

Related literature includes