locally cartesian closed (infinity,1)-category



An (∞,1)-category CC has finite (∞,1)-limits if it has a terminal object and for every object xXx \in X, the over-(∞,1)-category C /xC_{/x} has finite products.

We say that such a CC is locally cartesian closed if moreover C /xC_{/x} is a cartesian closed (∞,1)-category for every object xx. This is equivalent to asking that the pullback functor f *:C yC xf^*\colon C_{\y} \to C_{\x}, for any f:xyf\colon x\to y in CC, has a right adjoint Π f\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 (,1)(\infty,1)-category CC, the following are equivalent.

  1. CC is locally cartesian closed.
  2. (∞,1)-Colimits in CC are stable under pullback.
  3. CC admits a presentation by a combinatorial locally cartesian closed model category.
  4. CC admits a presentation by a right proper Cisinski model category.
  5. CC admits a presentation by a right proper left Bousfield localization of an injective model category of simplicial presheaves.

Since left adjoints preserve colimits, the first condition implies the second. The converse holds by the adjoint functor theorem since each slice of CC is locally presentable.

Suppose MM is a right proper Cisinski model category. Then pullback along a fibration preserves cofibrations (since they are the monomorphisms) and weak equivalences (since MM is right proper). Since MM 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).


Further equivalent characterizations of locally cartesian closed (,1)(\infty,1)-categories are in (Lurie, prop., lemma


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

Internal logic and homotopy type theory


Theorem 1 says in particular that every presentable and locally cartesian closed (,1)(\infinity,1)-category has a presentation by a type-theoretic model category. As discussed there, such provides the categorical semantics for homotopy type theory (without, possibly, the univalence axiom).

Therefore theorem 1 says in particular that “Every presentable locally cartesian closed (,1)(\infinity,1)-category interprets homotopy type theory.”

This includes in particular all (∞-stack-) (∞,1)-toposes (which should in addition satisfy univalence). See also at internal logic of an (∞,1)-topos.

It seems that Chris Kapulkin is close to establishing an actual equivalence, in a suitable sense, between homotopy type theories (without possibly univalence) and presentable locally Cartesian closed (,1)(\infty,1)-Categories, in higher analogy of the relation between type theory and category theory (see there for more).

The internal logic of (presentable) locally cartesian closed (,1)(\infty,1)-categories was explicitly conjectured in (Joyal 2011) to be a sort of homotopy type theory (specifically, that with intensional identity types and dependent products).


Characterizations of locally cartesial closed (,1)(\infty,1)-categories (as presentable (∞,1)-categories with universal colimits) are discussed in section 6.1 of

Early discussion in the context of homotopy type theory is in

where the conjecture is first stated that homotopy type theory has categorical semantics in locally Cartesian closed \infty-categories.

Denis-Charles Cisinski’s argument in theorem 1 above that every locally Cartesian closed (,1)(\infinity,1)-category admits a presentation by a type-theoretic model category is mentioned in print in section 2

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

For more on this see also the relevant sections at relation between type theory and category theory.

A discussion of object classifiers, univalent families, and model category presentations is the context of \infty-categories (and hence in categorical semantics for what should be homotopy type theory with univalent universes “weakly a la Tarski”) appeared also in

Revised on November 29, 2014 21:30:09 by Ingo Blechschmidt (