The HoTT reals coincide with the Escard\'o-Simpson reals
Logic in Computer Science
2017-06-20 v1 Category Theory
Logic
Abstract
Escard\'o and Simpson defined a notion of interval object by a universal property in any category with binary products. The Homotopy Type Theory book defines a higher-inductive notion of reals, and suggests that the interval may satisfy this universal property. We show that this is indeed the case in the category of sets of any universe. We also show that the type of HoTT reals is the least Cauchy complete subset of the Dedekind reals containing the rationals.
Keywords
Cite
@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}
}