Title: The HoTT reals coincide with the Escardó-Simpson reals,
Abstract: 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 reals is
the least Cauchy complete subset of the Dedekind reals containing the
rationals.