Homotopy Type Theory real numbers > history (Rev #16)

Definition

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

• computable real numbers

• sequentially Cauchy complete Archimedean ordered field

• Dedekind real numbers (disambiguation)

• Dedekind real closed intervals, where the Dedekind real numbers are the located Dedekind real closed intervals, and the computable real numbers are the Dedekind real closed intervals with a locator.

References

• Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)

• Mark Bridger, Real Analysis: A Constructive Approach Through Interval Arithmetic, Pure and Applied Undergraduate Texts 38, American Mathematical Society, 2019.