一句话：提出基于 Moore 路径的内涵 Martin-Löf 类型论模型，构造非截断模型且无需 Kan 填充条件。
本文为内涵 Martin-Löf 类型论引入一类新的模型。作者在 topos 中使用构造性有序代数，并用 Moore 路径的概念解释 identity types（同一类型）。通过考察一个特定的 gros topos，他们构造出一个非截断模型：任意深度的嵌套 identity type 都可以包含多于一个元素，而不仅仅在低维处有非平凡结构。与基于单纯集合和立方集合的既有非截断模型相比，该模型的主要特点是类型语义完全不需要 Kan 填充条件。该工作为类型论的高维模型提供了新视角，并展示了在无需 Kan 填充条件的情况下获得非截断语义的可能性。
This paper introduces a new family of models of intensional Martin-L\"of 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 cubical sets, the notion of model presented here is notable for avoiding any form of Kan filling condition in the semantics of types. Comment: This is a revised and expanded version of a paper with the same name that appeared in the proceedings of the 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)
@article{paperbot837,
title = {Models of Type Theory Based on Moore Paths},
author = {Ian Orton and Andrew M. Pitts},
journal = {Logical Methods in Computer Science},
volume = {Volume 15, Issue 1},
number = {Type theory and constructive...},
year = {2019},
doi = {10.23638/lmcs-15(1:2)2019}
}