The HoTT book reals coincide with the Escardó-Simpson reals
This is an announcement of a paper in the area of univalent type theory and exact real arithmetic.
Escardó 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 book reals is the least Cauchy complete
subset of the Dedekind reals containing the rationals.
Preprint is on the arXiv.
Somewhat stronger results can be found in Chapter 5 of my PhD thesis. I intend to publish these results at a later stage.