同类型论的非标准模型

同类型论是一种现代数学基础，引入单一性公理，特别适合研究其同伦数学及其通过证明助理的形式化。在更好地理解同类型论的数学含义方面，已构建并研究了各种模型。这里所指的模型是指具有适当性质的模型范畴，其实现各种类型论构造器和公理的功能。第一个例子是由卡普尔金--兰姆斯代尔--沃夫夫斯基所著称的单纯模型。至今，已构建了许多其他模型，归功于阿恩特、卡普尔金、兰姆斯代尔、沃伦和特别是舒尔曼的工作，最终证明了每个Grothendieck ∞-拓扑集都可以作为模型范畴的底层∞-范畴，来建模同类型论。在本文中，我们提出滤 quotients 构造作为构建同类型论进一步模型的新方法。具体而言，我们证明在轻微假设下，滤 quotients 构造保留实现各种类型论构造器和公理的模型范畴属性。另一方面，滤 quotients 构造不保留许多外部属性，这些属性具有集合论性质，如完整性、局部可表示性或可诱生成。结合这些，我们表明滤 quotients 构造保留同类型论的模型，并且可以产生尚未考虑过的模型，并表现出与任何既定模型都不同行为的特征。