Homotopy Type Theory Cauchy real numbers (disambiguation) > history (Rev #1)

Disambiguation page

There are many different types which are called Cauchy real numbers in the literature. These include:

• sequential Cauchy real numbers?, which is defined using Cauchy sequences of rational numbers.

• generalized Cauchy real numbers, which is defined using all Cauchy nets of rational numbers in a universe.

• modulated sequential Cauchy real numbers? and modulated generalized Cauchy real numbers?, where the modulus of convergence is structure rather than mere property

• HoTT real numbers?, which is defined as the free complete metric space generated by the rational numbers, and called the Cauchy real numbers in the HoTT book.

References

HoTT book

• Auke B. Booij, The HoTT reals coincide with the Escardó-Simpson reals, (https://arxiv.org/abs/1706.05956)
• Auke B. Booij, Extensional constructive real analysis via locators, (https://arxiv.org/abs/1805.06781)