An interpretation of dependent type theory in a model category of locally cartesian closed categories

TL;DR

This paper develops a new semantic framework for dependent type theory by modeling the entire category of locally cartesian closed categories as a model category, enabling a global interpretation that can be sliced to recover traditional models.

Contribution

It introduces the 'gros' semantics, modeling all lcc categories collectively as a model category, extending the interpretation of dependent type theory beyond individual categories.

Findings

Constructed a model category of lcc sketches.

Derived model categories of strict lcc categories.

Provided a coherence solution via algebraically cofibrant objects.

Abstract

Locally cartesian closed (lcc) categories are natural categorical models of extensional dependent type theory. This paper introduces the "gros" semantics in the category of lcc categories: Instead of constructing an interpretation in a given individual lcc category, we show that also the category of all lcc categories can be endowed with the structure of a model of dependent type theory. The original interpretation in an individual lcc category can then be recovered by slicing. As in the original interpretation, we face the issue of coherence: Categorical structure is usually preserved by functors only up to isomorphism, whereas syntactic substitution commutes strictly with all type theoretic structure. Our solution involves a suitable presentation of the higher category of lcc categories as model category. To that end, we construct a model category of lcc sketches, from which we obtain by the formalism of algebraically (co)fibrant objects model categories of strict lcc categories and then algebraically cofibrant strict lcc categories. The latter is our model of dependent type theory.