有效拓扑斯中函数外延性的同伦理论模型
计算机科学中的逻辑
2018-03-13 v2 范畴论
摘要
我们提出一种在初等拓扑斯的全子范畴上构造 Quillen 模型结构的方法，始于带连接的区间对象和某种支配。该方法的优势在于不要求底层拓扑斯是余完备的。所得的模型范畴结构产生了具有恒等类型、- 和 -类型以及函数外延性的同伦类型论模型。我们将该方法应用于带区间对象 的有效拓扑斯。在所得模型结构中，我们将一致有居对象识别为可缩对象，并证明离散对象是 fibrant 的。此外，我们证明离散反射的单位是同伦等价，且 fibrant assemblies 的同伦范畴等价于 modest sets 范畴。我们将我们的工作与 Jaap van Oosten 在有效拓扑斯上构造的路径对象范畴进行比较。
引用
@article{arxiv.1701.08369,
title = {A homotopy-theoretic model of function extensionality in the effective topos},
author = {Daniil Frumin and Benno van den Berg},
journal= {arXiv preprint arXiv:1701.08369},
year = {2018}
}
备注
v2: The section "A non-contractible uniform object." was removed due to an error in Lemma 6.5, Proposition 7.3 was changed to account for the fact that only the "only if" direction holds