HoTT 实数与 Escardó-Simpson 实数一致
计算机科学中的逻辑
2017-06-20 v1 范畴论
逻辑
摘要
Escardó 和 Simpson 在任意具有二元积的范畴中通过泛性质定义了区间对象的概念。同伦类型论（HoTT）一书定义了实数的高阶归纳概念，并指出该区间可能满足此泛性质。我们证明，在任意宇宙的集合范畴中，情况确实如此。我们还证明了 HoTT 实数类型是包含有理数的 Dedekind 实数中最小的 Cauchy 完备子集。
引用
@article{arxiv.1706.05956,
title = {The HoTT reals coincide with the Escard\'o-Simpson reals},
author = {Auke Bart Booij},
journal= {arXiv preprint arXiv:1706.05956},
year = {2017}
}