论文标题
在本地笛卡尔封闭类别的模型类别中对依赖类型理论的解释
An interpretation of dependent type theory in a model category of locally cartesian closed categories
论文作者
论文摘要
本地笛卡尔封闭（LCC）类别是延伸依赖类型理论的自然分类模型。本文在LCC类别的类别中介绍了“ GROS”语义：而不是在给定的LCC类别中构建解释，而是表明所有LCC类别的类别也可以赋予依赖类型理论模型的结构。然后可以通过切片恢复单个LCC类别中的原始解释。与原始解释一样，我们面临着连贯性的问题：分类结构通常仅由函子保留，直到同构为异构，而句法替代则严格使用所有类型的理论结构。我们的解决方案涉及将LCC类别的较高类别类别作为模型类别的适当呈现。为此，我们构建了LCC草图的模型类别，我们从该模型中通过代数（CO）的形式主义获得严格LCC类别的模型类别，然后是代数合并的严格LCC类别。后者是我们的依赖类型理论的模型。
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.
