We say that such a is locally cartesian closed if moreover is a cartesian closed (∞,1)-category for every object . This is equivalent to asking that the pullback functor , for any in , has a right adjoint .
The internal logic of locally cartesian closed -categories is conjectured (Joyal2011) to be a sort of homotopy type theory (specifically, that with intensional identity types and dependent products). For more on this see relation between type theory and category theory.
See also internal logic of an (∞,1)-topos.
The following theorem should be compared with the fact that every locally presentable (∞,1)-category admits a presentation by a Cisinski model category, indeed by a left Bousfield localization of a global model structure on simplicial presheaves.
For a locally presentable -category , the following are equivalent.
I have a question here. The third condition says that admits a presentation as a left Bousefield localization of a category of simplicial presheaves with the projective model structure. The fifth conditions claims this for a category of simplical presheaves with the injective model structure. How can that be?
Answer (Dylan W.): I believe the injective and projective model structures on simplicial presheaves are Quillen equivalent.
Suppose is a right proper Cisinski model category. Then pullback along a fibration preserves cofibrations (since they are the monomorphisms) and weak equivalences (since is right proper). Since is a locally cartesian closed 1-category, pullback also has a right adjoint, so it is a left Quillen functor; thus the fourth condition implies the third. Since left Quillen functors preserve homotopy colimits, the third condition implies the second.
Clearly the fifth condition implies the fourth, so it suffices to show that the second condition implies the fifth. For that, see this blog comment by Denis-Charles Cisinski. An alternative proof can be found in (Gepner-Kock).
Further equivalent characterizations of locally cartesian closed -categories are in (Lurie, prop. 220.127.116.11, lemma 18.104.22.168)
cartesian closed (∞,1)-category, locally cartesian closed (∞,1)-category
Discussion in the context of homotopy type theory is in
A discussion of object classifiers, univalent families, and model category presentations is in