UniMath 中圆的构造
逻辑
2020-11-19 v2 计算机科学中的逻辑
代数拓扑
摘要
我们证明 -挠子(torsor)的类型 具有圆的依赖泛性质，该性质在唯一同伦等价意义下刻画了圆。该构造使用了 Voevodsky 的 univalence 公理与命题截断，给出了一个不依赖于高阶归纳类型的独立圆构造。
引用
@article{arxiv.1910.01856,
title = {Construction of the Circle in UniMath},
author = {Marc Bezem and Ulrik Buchholtz and Daniel R. Grayson and Michael Shulman},
journal= {arXiv preprint arXiv:1910.01856},
year = {2020}
}
备注
27 pages; many improvements thanks to referee comments; added Shulman as co-author, who helped write a new section on the interpretation in higher toposes