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

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

References

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