Homotopy Type Theory Cauchy real numbers (disambiguation) > history (changes)

• Cauchy real numbers, which is sometimes defined using Cauchy sequences of a dense integral subdomain of the rational numbers.

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

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

• HoTT book real numbers, which is defined as the initial Cauchy structure, and called the Cauchy real numbers in the HoTT book.

See also

• real numbers for other types of real numbers

References

• Auke B. Booij, The HoTT reals coincide with the Escardó-Simpson reals, (abs:1706.05956)
• Auke B. Booij, Extensional constructive real analysis via locators, (abs:1805.06781)
• Auke B. Booij, Analysis in univalent type theory (pdf)
• Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)