nLab
locally cartesian closed category

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, $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.

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.

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.

References

• Conduché, François. 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'eom. Diff'erentielle, 20 (1979) 281–296.

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