同伦类型论模型中的内部宇宙
计算机科学中的逻辑
2019-12-18 v4
摘要
我们首先回顾同伦类型论各种模型中宇宙本质上是全局性的特征，这阻碍了使用构造这些模型的前层topos的内部语言对其性质进行直接公理化。我们通过用一种模态算子扩展内部语言来表达全局元素的性质，从而绕过了这一问题。在此设定下，我们展示了如何从区间是tiny（微小）的这一假设出发，构造一个分类Cohen-Coquand-Huber-Mörtberg (CCHM) 从其立方集模型提出的纤维化概念的宇宙——立方集中的区间确实具有这一性质。这导致了在该我们称之为crisp类型论的内部，对同伦类型论的该模型及相关模型的一种初等公理化。
引用
@article{arxiv.1801.07664,
title = {Internal Universes in Models of Homotopy Type Theory},
author = {Daniel R. Licata and Ian Orton and Andrew M. Pitts and Bas Spitters},
journal= {arXiv preprint arXiv:1801.07664},
year = {2019}
}
备注
In H. Kirchner (ed), Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), Leibniz International Proceedings in Informatics (LIPIcs), Vol. 108, pp. 22:1-22:17, 2018