等同类型的拓扑与单纯模型

在本文中，我们在拓扑空间范畴Top和单纯集合范畴SSet中，为Martin-Löf类型论的等同类型构造了新的范畴模型。我们的工作建立在Awodey和Warren早期研究的基础之上，该研究指出，解释等同类型的合适环境应该是一个配备有Bousfield-Quillen意义下弱分解系统的范畴。事实证明，由于涉及替换下稳定性的一些微妙的相干性问题，这对于一个可靠的模型来说还不够充分；因此，我们的首要任务是引入一种稍微丰富的结构——我们称之为等同类型的同伦论模型——并证明这对于可靠的解释是充分的。现在，尽管Top和SSet都是赋予弱分解系统——甚至完整的Quillen模型结构——的范畴，但要展示同伦论模型所需的附加结构却相当困难。然而，我们感兴趣的范畴具有许多共同特征，对这些特征进行抽象引出了路径对象范畴的概念。这是一个相对简单的公理化框架，但它足够强大以允许构造同伦论模型。现在，通过在Top和SSet上展示合适的路径对象结构，我们赋予这些范畴同伦论模型的结构：以此方式，获得了所需的等同类型的拓扑与单纯模型。