同伦类型论中的实射影空间
代数拓扑
2017-04-20 v1
摘要
同伦类型论是利用其同伦模型的一个 Martin-Löf 类型论版本。特别地，我们可以使用并构造同伦论中的对象，并利用高阶归纳类型对它们进行推理。在本文中，我们构造了同伦论中的关键角色——实射影空间，作为同伦类型论中的某些高阶归纳类型。RP(n) 的经典定义，即识别 n-球面上对径点的商空间，不能直接翻译到同伦类型论中。相反，我们通过关于 n 的归纳同时定义 RP(n) 及其 2-元素集合的典范丛。作为基例，我们取 RP(-1) 为空类型。在归纳步骤中，我们取 RP(n+1) 为 RP(n) 的典范丛的投影映射的映射锥，并利用其泛性质与单值公理来定义 RP(n+1) 上的典范丛。通过证明 RP(n) 的典范丛的全空间是 n-球面，我们重新得到了 RP(n+1) 的经典描述：即在 RP(n) 上附加一个 (n+1)-胞腔。无限维实射影空间定义为具有典范包含映射的 RP(n) 的顺序余极限，它等价于 Eilenberg-MacLane 空间 K(Z/2Z,1)，此处它作为由 2-元素类型组成的宇宙的子类型出现。事实上，无限维射影空间分类 0-球面丛，可视为合成线丛。这些在同伦类型论中的构造进一步说明了同伦类型论的效用，包括类型论与同伦论思想的相互作用。
引用
@article{arxiv.1704.05770,
title = {The real projective spaces in homotopy type theory},
author = {Ulrik Buchholtz and Egbert Rijke},
journal= {arXiv preprint arXiv:1704.05770},
year = {2017}
}
备注
8 pages, to appear in proceedings of LICS 2017