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 $C$ has a terminal object, then $C$ is itself cartesian closed and in fact has all finite limits; 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 a dependent product.

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

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.

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

• 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.

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

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

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)