A locally cartesian closed category is a category whose slice categories are all cartesian closed. If has a terminal object, then is itself cartesian closed and in fact has all finite limits; often this requirement is included in the definition.
Equivalently, is a category with pullbacks (and a terminal object, if required) such that each base change functor has a right adjoint , 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 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 the base change functor has a right adjoint. This includes , , and the category of crossed complexes; in the latter two cases, it is necessary and sufficient for to be a fibration, while in it is sufficient for to be a fibration or an opfibration.
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.