nLab
locally cartesian closed (infinity,1)-category

Definition

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^{*}:C_y\to C_x$, for any $f:x\to y$ in $C$, has a right adjoint ${\Pi }_f$.

Examples

• Every (Grothendieck) (∞,1)-topos is locally cartesian closed. This follows from the universality of colimits and the adjoint functor theorem.

Properties

Internal logic

The internal logic of locally cartesian closed $(\mathrm{\infty },1)$-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.

Presentations

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.

Theorem

For a locally presentable $(\mathrm{\infty },1)$-category $C$, the following are equivalent.

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

I have a question here. The third condition says that $C$ 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.

Proof

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

Remark

Further equivalent characterizations of locally cartesian closed $(\mathrm{\infty },1)$-categories are in (Lurie, prop. 6.1.1.4, lemma 6.1.3.3)

Related concepts

• cartesian closed category, locally cartesian closed category

• cartesian closed functor, locally cartesian closed functor

• cartesian closed model category, locally cartesian closed model category

• cartesian closed (∞,1)-category, locally cartesian closed (∞,1)-category

References

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

• Jacob Lurie, Higher Topos Theory

Discussion in the context of homotopy type theory is in

• André Joyal, Remarks on homotopical logic, Oberwolfach (2011) (pdf)

A discussion of object classifiers, univalent families, and model category presentations is in

• David Gepner, Joachim Kock, “Univalence in locally cartesian closed ∞-categories”, arXiv