locally cartesian closed model category

cartesian closed model category, locally cartesian closed model category

- Strom model structure?

on chain complexes/model structure on cosimplicial abelian groups

related by the Dold-Kan correspondence

model structure on differential graded-commutative superalgebras

on dendroidal sets, for dendroidal complete Segal spaces, for dendroidal Cartesian fibrations

model structure for (2,1)-sheaves/for stacks

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.

A model category $\mathcal{C}$ which is additionally a locally cartesian closed category is called a **locally cartesian closed model category** if for any fibration $g\colon A\to B$ between fibrant objects, the dependent product adjunction

$g^* : \mathcal{C}/B \rightleftarrows \mathcal{C}/A : \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 $A \to B$ as above the internal hom adjunction in the slice category over $B$

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

is a Quillen adjunction.

Any right proper model category which is locally cartesian closed and in which the cofibrations are the monomorphisms is a locally cartesian closed model category. This includes the classical model structure on simplicial sets, as well as the injective global model structure on simplicial presheaves. More generally, it includes any right proper Cisinski model structure.

It is easy to see that the $(\infty,1)$-category presented by a locally cartesian closed model category is itself locally cartesian closed. 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 locally cartesian closed (infinity,1)-category for the proof.

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

Last revised on May 10, 2012 at 20:24:04. See the history of this page for a list of all contributions to it.