equivalences in/of $(\infty,1)$-categories
An (∞,1)-category $C$ has finite (∞,1)-limits if it has a terminal object and for every object $x \in X$, the over-(∞,1)-category $C_{/x}$ has finite products.
We say that such a $C$ is locally cartesian closed if moreover $C_{/x}$ is a cartesian closed (∞,1)-category for every object $x$. This is equivalent to asking that the pullback functor $f^*\colon C_{\y} \to C_{\x}$, for any $f\colon x\to y$ in $C$, has a right adjoint $\Pi_f$.
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 $(\infty,1)$-category $C$, the following are equivalent.
Since left adjoints preserve colimits, the first condition implies the second. The converse holds by the adjoint functor theorem since each slice of $C$ is locally presentable.
Suppose $M$ is a right proper Cisinski model category. Then pullback along a fibration preserves cofibrations (since they are the monomorphisms) and weak equivalences (since $M$ is right proper). Since $M$ 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 12, Thm 7.10).
Further equivalent characterizations of locally cartesian closed $(\infty,1)$-categories are in (Lurie, prop. 6.1.1.4, lemma 6.1.3.3)
Comparing the third and the fifth item in theorem 1 notice that the projective and the injective model structure on simplicial presheaves are Quillen equivalent (as discussed at model structure on functors.)
It is expected that the internal logic of locally cartesian closed $(\infty,1)$-categories should be a sort of homotopy type theory (specifically, that with intensional identity types and dependent products), in higher analogy with the relation between type theory and category theory.
Ideally, this should involve two directions: interpretation of type theory in such $(\infty,1)$-categories, and construction of such $(\infty,1)$-categories from syntax.
For the first direction, Theorem 1 says in particular that every locally presentable and locally cartesian closed $(\infinity,1)$-category has a presentation by a type-theoretic model category. As discussed there, this provides the categorical semantics for homotopy type theory (without in general the univalence axiom). Together, this yields:
(Cisinski, Shulman) Every locally presentable locally cartesian closed $(\infinity,1)$-category admits an interpretation of type theory with $\Sigma$-types, $\Pi$-types, and $\mathrm{Id}$-types.
This includes in particular all (∞-stack-) (∞,1)-toposes, which should in addition possess univalent universes. See also internal logic of an (∞,1)-topos.
An explicit statement in the second direction was conjectured in (Joyal 2011), and established in Chris Kapulkin’s PhD thesis (see Kapulkin 14):
(Kapulkin) If T is any dependent type theory with (at least) $\Sigma$-types, $\Pi$-types, and $\mathrm{Id}$-types, then the simplicial localisation of its classifying category $\mathrm{Cl}(\mathbf{T})$ is a locally cartesian closed $(\infty,1)$-category.
However, this “syntactic $(\infty,1)$-category” will not in general be locally presentable, lacking appropriate colimits. There is thus a mismatch between the two best statements we have at present, for the two directions of the internal language correspondence.
cartesian closed category, locally cartesian closed category
cartesian closed model category, locally cartesian closed model category
cartesian closed (∞,1)-category, locally cartesian closed (∞,1)-category
Characterizations of locally presentable locally cartesian closed $(\infty,1)$-categories (as locally presentable (∞,1)-categories with universal colimits) are discussed in section 6.1 of
Early discussion in the context of homotopy type theory is in
proposing homotopy type theory as an internal language for locally cartesian closed $\infty$-categories.
Denis-Charles Cisinski’s argument in Theorem 1 above, that every locally presentable locally cartesian closed $(\infinity,1)$-category admits a presentation by a type-theoretic model category, originally appeared on the Cafélog comment](http://golem.ph.utexas.edu/category/2012/05/the_mysterious_nature_of_right.html#c041306)) and is mentioned in print in Examples 2.16 of
which gives a detailed account of the categorical semantics of homotopy type theory in type-theoretic model categories such as those presenting locally cartesian closed $(\infty,1)$-categories.
For more on this see also the relevant sections at relation between type theory and category theory.
Discussion of the converse direction, obtaining locally cartesian closed $(\infty,1)$-categories as syntactic categories of homotopy type theories is in
A discussion of object classifiers, univalent families, and model category presentations is the context of $(\infty,1)$-categories (and hence in categorical semantics for what should be homotopy type theory with univalent universes “weakly a la Tarski”) appeared also in