文章基本信息

标题：Models of Type Theory Based on Moore Paths
本地全文：下载
作者：Ian Orton ; Andrew M. Pitts
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2017
卷号：84
页码：28:1-28:16
DOI：10.4230/LIPIcs.FSCD.2017.28
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：This paper introduces a new family of models of intensional Martin-Löf type theory. We use constructive ordered algebra in toposes. Identity types in the models are given by a notion of Moore path. By considering a particular gros topos, we show that there is such a model that is non-truncated, i.e. contains non-trivial structure at all dimensions. In other words, in this model a type in a nested sequence of identity types can contain more than one element, no matter how great the degree of nesting. Although inspired by existing non-truncated models of type theory based on simplicial and on cubical sets, the notion of model presented here is notable for avoiding any form of Kan filling condition in the semantics of types.
关键词：dependent type theory; homotopy theory; Moore path; topos