nLab
locally cartesian closed category

Definition

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

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

Equivalently, a locally cartesian category $C$ is a category with pullbacks (and a terminal object, if required) such that each base change functor $f^{*}:C/y\to C/x$ has a right adjoint ${\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.

Properties

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

Proposition

Let $𝒞$ be a category with pullbacks that has all dependent products ${\prod }_{•}$, equivalently that every morphism $f:E\to X$ in $𝒞$ induces an adjoint triple

$${𝒞}_{/E}\stackrel{\stackrel{\sum _f}{\to }}{\stackrel{\stackrel{f^{*}}{\leftarrow }}{\underset{\prod _f}{\to }}}{𝒞}_{/X}.$$\mathcal{C}_{/E} \stackrel{\overset{\sum_f}{\to}}{\stackrel{\overset{f^*}{\leftarrow}}{\underset{\prod_f}{\to}}} \mathcal{C}_{/X} \,.

Then the internal hom in a slice ${𝒞}_{/X}$ exists and is given by

$$[⟨E\stackrel{f}{\to }X⟩,-{]}_{{𝒞}_{/X}}\simeq \prod _f\circ f^{*}.$$[\langle E \stackrel{f}{\to} X\rangle \; ,\; -]_{\mathcal{C}_{/X}} \simeq \prod_f \circ f^* \,.

Proof

By the discusson at overcategory-Limits and colimits the product in the slice ${𝒞}_{/X}$ of two objects $⟨E_1\stackrel{f_1}{\to }X⟩$ and $⟨E_1\stackrel{f_2}{\to }X⟩$ is given by the pullback $f_1^{*}{E}_2=f_2^{*}{E}_1$ in $𝒞$, regarded again as a morphism over $X$. More formally this means that the product with $⟨E\stackrel{f}{\to }X⟩$ is given by the composite

$$(-){\times }_{{𝒞}_{/X}}⟨E\stackrel{f}{\to }X⟩:{𝒞}_{/X}\stackrel{f^{*}}{\to }{𝒞}_{/E}\stackrel{\sum _f}{\to }{𝒞}_{/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 $f$ with the dependent sum along $f$. 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}\stackrel{\prod _f}{\leftarrow }{𝒞}_{/E}\stackrel{f^{*}}{\leftarrow }{𝒞}_{/X}:[⟨E\stackrel{f}{\to }X⟩,-{]}_{{𝒞}_{/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}} \,.

Proposition

If for a category $𝒞$ every slice category is a cartesian closed category, then for every morphism $f:X\to Y$ in $𝒞$ the dependent product ${\prod }_f$ exists and is given on an object $E\stackrel{p}{\to }X$ by the pullback

$$\begin{array}{ccc}\prod _f⟨E\stackrel{p}{\to }X⟩& \to & [⟨X\stackrel{f}{\to }Y⟩,⟨E\stackrel{p}{\to }X\stackrel{f}{\to }Y⟩{]}_{{𝒞}_{/Y}}\\ \downarrow & & \downarrow \\ Y& \stackrel{\overline{\mathrm{id}}}{\to }& [⟨X\stackrel{f}{\to }Y⟩,⟨X\stackrel{f}{\to }Y⟩{]}_{{𝒞}_{/Y}}\end{array}$$\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}$, where the bottom morphism is the adjunct of

$$Y{\times }_{{𝒞}_{/Y}}⟨X\stackrel{f}{\to }Y⟩\simeq ⟨X\stackrel{f}{\to }Y⟩\stackrel{\mathrm{id}}{\to }⟨X\stackrel{f}{\to }Y⟩.$$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 \,.

Proof

It is sufficient to check the $(f^{*}⊣{\prod }_f)$-adjunction hom set-natural isomorphism

$${𝒞}_{/Y}(⟨F\stackrel{}{\to }Y⟩,\prod _f⟨E\stackrel{p}{\to }X⟩)\simeq {𝒞}_{/X}(f^{*}⟨F\stackrel{}{\to }Y⟩,⟨E\stackrel{p}{\to }X⟩),$$\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\stackrel{}{\to }Y⟩$.

Since the hom functor ${𝒞}_{/Y}(⟨F\stackrel{}{\to }Y⟩,-)$ preserves limits and hence pullbacks, the expression on the left is exhibited as the pullback

$$\begin{array}{ccc}{𝒞}_{/Y}(⟨F\stackrel{}{\to }Y⟩,\prod _f⟨E\stackrel{p}{\to }X⟩& \to & {𝒞}_{/Y}(⟨F\stackrel{}{\to }Y⟩,[⟨X\stackrel{f}{\to }Y⟩,⟨E\stackrel{p}{\to }X\stackrel{f}{\to }Y⟩{]}_{{𝒞}_{/Y}})\\ \downarrow & & \downarrow \\ *& \stackrel{}{\to }& {𝒞}_{/Y}(⟨F\stackrel{}{\to }Y⟩,[⟨X\stackrel{f}{\to }Y⟩,⟨X\stackrel{f}{\to }Y⟩{]}_{{𝒞}_{/Y}})\end{array}$$\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 $((-){\times }_{{𝒞}_{/Y}}⟨X\stackrel{f}{\to }Y⟩⊣[⟨X\stackrel{f}{\to }Y⟩,-{]}_{{𝒞}_{/Y}})$-adjunction this is equivalently

$$\begin{array}{ccc}{𝒞}_{/Y}(⟨F\stackrel{}{\to }Y⟩,\prod _f⟨E\stackrel{p}{\to }X⟩& \to & {𝒞}_{/Y}(⟨F\stackrel{}{\to }Y⟩{\times }_{{𝒞}_{/Y}}⟨X\stackrel{f}{\to }Y⟩,⟨E\stackrel{p}{\to }X\stackrel{f}{\to }Y⟩)\\ \downarrow & & \downarrow \\ *& \stackrel{}{\to }& {𝒞}_{/Y}(⟨F\stackrel{}{\to }Y⟩{\times }_{{𝒞}_{/Y}}⟨X\stackrel{f}{\to }Y⟩,⟨X\stackrel{f}{\to }Y⟩)\end{array}.$$\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\to Y⟩,⟨E\stackrel{p}{\to }X⟩)$.

Proposition

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

Proof

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

$$(C/Y)/(f:X\to Y)\simeq C/X$$(C/Y)/(f \colon X \to Y) \simeq C/X

whence the statement immediately follows.

Proposition

If $C$ is locally cartesian closed (and has a terminal object), then the pullback functor $X\times -:C\to C/X$ preserves both finite products and exponentials up to isomorphism.

Proof

Clearly $X\times -:C\to C/x$, being right adjoint to the forgetful functor ${\sum }_X:C/X\to C$, preserves limits, hence it preserves finite products in particular.

Let $\varphi :A\to X$ be any morphism. From the pullback diagram

$$\begin{array}{ccc}A\times Z& \stackrel{\varphi \times 1}{\to }& X\times Z\\ {}_{{\pi }_A}\downarrow & & {\downarrow }_{{\pi }_X}\\ A& \underset{\varphi }{\to }& X\end{array}$$\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{\times }_X(X\times Z)\cong A\times Z$, seen as an object over $X$ via $\varphi \circ {\pi }_A:A\times Z\to X$. Thus arrows in the slice $C/X$ of the form

$$A{\times }_X(X\times Z)\to X\times Y$$A \times_X (X \times Z) \to X \times Y

are in natural bijection with arrows in $C$ of the form

$$A\times Z\stackrel{⟨\varphi \circ {\pi }_A,g⟩}{\to }X\times Y$$A \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/X$ of the form

$$A\stackrel{⟨\varphi ,\tilde{g}⟩}{\to }X\times Y^Z$$A \stackrel{\langle \phi, \tilde{g} \rangle}{\to} X \times Y^Z

(where $\tilde{g}:A\to Y^Z$ is obtained by currying $g:A\times Z\to Y$ in $C$). This proves that $X\times -:C\to C/x$ preserves exponentials.

Corollary

For any $f:X\to Y$ in $C$, the base change $f^{*}:C/Y\to C/X$ preserves exponentials. In other words, the dependent sum functor ${\sum }_f$ and the dependent product functor ${\prod }_f$ satisfy Frobenius reciprocity.

Proof

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

$$C/Y\to (C/Y)/(f:X\to Y)\simeq C/X$$C/Y \to (C/Y)/(f \colon X \to Y) \simeq C/X

is identified with the pullback functor $f^{*}:C/Y\to C/X$.

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

Proposition

If $C$ is a category with finite limits, then it is locally cartesian closed precisely if regarded as an $C$-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.

Proposition

Let

$$\begin{array}{ccccc}X& & & & A\\ & {}_{\varphi }\searrow & & {\swarrow }_c\\ & & B\end{array}$$\array{ X &&&& A \\ & {}_{\mathllap{\phi}}\searrow && \swarrow_{\mathrlap{c}} \\ && B }

be two display maps. Then the category theoretic identification

$$[X,A{]}_B=\prod _{\varphi }{\varphi }^{*}⟨A\stackrel{c}{\to }X⟩$$[X,A]_{B} = \prod_\phi \phi^* \langle A \stackrel{c}{\to} X\rangle

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

$$b:B⊢X(b)\to A(b):\mathrm{Type}{=}_{\mathrm{def}}b:B⊢\prod _{x:X(b)}A(\varphi (x)).$$b : B \vdash X(b) \to A(b) : Type \;\;\; =_{def} \;\;\; b : B \vdash \prod_{x : X(b)} A(\phi(x)) \,.

Remark

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 $B$) = ( collection of sections of the pullback of $A$ to $X$ )

Proof

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

$$b:B⊢A(b):\mathrm{Type},$$b : B \vdash A(b) : Type \,,

the pullback $f^{*}⟨A\to B⟩$ is expressed by substitution

$$x:X⊢A(\varphi (x)):\mathrm{Type}$$x : X \vdash A(\phi(x)) : Type

and next the dependent product ${\prod }_{\varphi }{\varphi }^{*}⟨A\to B⟩$ by

$$b:B⊢\prod _{x:X(b)}A(\varphi (x)):\mathrm{Type}.$$b : B \vdash \prod_{x : X(b)} A(\phi(x)) : Type \,.

Now on the right $\varphi (x){=}_{\mathrm{def}}b$, formally because $\varphi$ is equivalently the projection ${\mathrm{pr}}_1$ out of $X$ expressed as the direct sum

$$\frac{(b,x):\sum _{b:B}X(b)}{{\mathrm{pr}}_1(b,x){=}_{\mathrm{def}}b{=}_{\mathrm{def}}\varphi (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⊢\prod _{x:X(b)}A(b):\mathrm{Type}.$$b : B \vdash \prod_{x : X(b)} A(b) : Type \,.

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

$$b:B⊢X(b)\to A(b):\mathrm{Type}.$$b : B \vdash X(b) \to A(b) : Type \,.

which expresses the internal hom in the slice over $B$.

Internal logic

The internal logic of locally cartesian closed categories is an extensional form of dependent type theory. In particular, the dependent product ${\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 $f$ the base change functor $f^{*}:C/y\to C/x$ has a right adjoint. This includes $\mathrm{Cat}$, $\mathrm{Gpd}$, and the category of crossed complexes; in the latter two cases, it is necessary and sufficient for $f$ to be a fibration, while in $\mathrm{Cat}$ it is sufficient for $f$ to be a fibration or an opfibration.

Examples

Proposition

Every sheaf topos is locally cartesian closed.

Proof

By Giraud's theorem, in a sheaf topos pullbacks preserve colimits. With the adjoint functor theorem this implies that for every morphism $f:X\to Y$, the pullback functor $f^{*}:{𝒞}_{/Y}\to {𝒞}_{/X}$ has a right adjoint ${\prod }_f$. By prop. 1 this yields the local cartesian closure.

Related concepts

• cartesian closed category, locally cartesian closed category

• cartesian closed functor, locally cartesian closed functor

• cartesian closed model category, locally cartesian closed model category

• cartesian closed (∞,1)-category locally cartesian closed (∞,1)-category

References

A standard textbook account is around corollary A1.5.3 in

• Peter Johnstone, Sketches of an Elephant

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

• Peter Freyd, Aspects of topoi, Bull. Australian Math. Soc. 7 (1972), 1-76.

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

• R. A. G. Seely, Locally cartesian closed categories and type theory, Math. Proc. Camb. Phil. Soc. (1984) 95 (pdf)

Related literature includes

• Marta Bunge, and Susan Niefield, Exponentiability and single universes J. Pure Appl. Algebra 148 (2000) 217–250.

• François Conduché, Au sujet de l’existence d’adjoints à droite aux foncteurs “image réciproque” dans la catégorie des catégories (French) C. R. Acad. Sci. Paris Sér. A-B 275 (1972), A891–A894.

• J. Howie, Pullback functors and crossed complexes , Cahiers Topologie Géom. Différentielle, 20 (1979) 281–296.