nLab locally cartesian closed model category

Idea

A locally cartesian closed model category is a locally cartesian closed category which is equipped with the structure of a model category in a compatible way, namely such that all right base change-adjunctions along fibrations are Quillen adjunctions, hence such that all their dependent product-functors are right Quillen functors.

Remark

(relation to cartesian closed model categories)
Beware that, despite the terminology, the axioms on a locally cartesian closed model category (Def. ) do not imply that the underlying model category (or any of its slice model categories) is a cartesian closed model category – and in most examples this is not the case. Namely, the axioms here (2) only require Quillen functors in one variable (the second variable for internal homs, with the other variable a fixed fibrant object) where those of a cartesian closed model category require Quillen bifunctors.

Definition

Definition

(locally cartesian closed model category)
A locally cartesian closed model category is

• a model category $\mathcal{C}$,

• whose underlying category is a locally cartesian closed category

• such that for every fibration between fibrant objects

  (1)$$\array{ A &\underoverset{\;\;\;\;\;\in Fib\;\;\;\;\;}{g}{\longrightarrow}& B \\ && \big\downarrow {}^{\mathrlap{\in Fib}} \\ && \ast }$$

  the dependent product/base change adjunction

  $$g^* \;\colon\; \mathcal{C}/B \rightleftarrows \mathcal{C}/A \;\colon\; \Pi_g$$

  is a Quillen adjunction between the corresponding slice model structures.

Concretely, this means that both cofibrations and trivial cofibrations are stable under pullback along fibrations between fibrant objects.

Equivalently this means that for all fibrations $A \to B$ the internal hom adjunction in the slice category over $B$

(2)$$(-) \times_{\mathcal{C}/_B} A \;:\; \mathcal{C}/_B \rightleftarrows \mathcal{C}/_B \;:\; [A, -]_{\mathcal{C}/_B}$$

is a Quillen adjunction.

Examples

Example

Any right proper model category whose underlying category is locally cartesian closed and in which the cofibrations are the monomorphisms is a locally cartesian closed model category.

Proof

The fiber product/pullback functor $g^\ast$

• is a left adjoint by local cartesian closure of the underlying category,

• preserves cofibrations because these are the monomorphisms and hence are preserved by pullback (by this prop.),

• preserves weak equivalences, and hence acyclic cofibrations by the previous item, due to right properness – using here the assumption (1) that $g$ is a fibration.

In summary this means that $g^\ast$ is a left Quillen functor.

Example

Example subsumes the following classes of examples, in increasing generality:

• the classical model structure on simplicial sets,

• any injective global model structure on simplicial presheaves,

• any injective local model structure on simplicial presheaves whose weak equivalences are detected stalk-wise (by the discussion there),

• any right proper Cisinski model structure.

Versus locally cartesian closed $(\infty,1)$-categories

It is easy to see that the $(\infty,1)$-category presented by a locally cartesian closed model category is itself locally cartesian closed: With the assumption (1) that $g$ is a fibration between fibrant objects, it follows (by this Prop) that pullback along $g$ models the correct homotopy pullback.

Conversely, any locally presentable locally cartesian closed $(\infty,1)$-category can be presented by some right proper Cisinski model category, which is therefore a locally cartesian closed model category; see there for the proof.

Versus homotopy type theories

• Modulo questions of strictness and coherence (see at initiality conjecture for details), locally cartesian closed model categories provide categorical semantics for homotopy type theory with function extensionality.

Related concepts

• cartesian closed category, locally cartesian closed category

• cartesian closed functor, locally cartesian closed functor

• cartesian closed model category

• locally cartesian closed enriched category

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