# The HoTT reals coincide with the Escard\'o-Simpson reals

## TL;DR

This paper proves that the HoTT reals and the Escardó-Simpson reals are equivalent in the category of sets, establishing their universal property and their characterization as the least Cauchy complete subset of Dedekind reals containing the rationals.

## Contribution

It demonstrates the equivalence of HoTT reals and Escardó-Simpson reals and characterizes the HoTT reals as the minimal Cauchy complete subset of Dedekind reals.

## Key findings

- HoTT reals satisfy the universal property of the interval object.
- The HoTT reals coincide with the least Cauchy complete subset of Dedekind reals.
- The equivalence holds in the category of sets of any universe.

## 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.