## Definition ## The type of __real numbers__ $\mathbb{R}$ is a [[locally (-1)-connected]] [[Hausdorff]] [[sober]] [[Archimedean ordered field]] with a [[compact]] [[real unit interval]] $[0, 1]$. ## Other types called 'real numbers' ## There are many other different types which are called real numbers in the literature, many of which are do not satisfy the same properties as listed above for the real numbers. 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, [[HoTT book|Homotopy Type Theory – Univalent Foundations of Mathematics]] (2013) * Andrej Bauer and Paul Taylor, [The Dedekind Reals in Abstract Stone Duality](https://www.paultaylor.eu/ASD/dedras/index.html) * Mark Bridger, [Real Analysis: A Constructive Approach Through Interval Arithmetic](https://bookstore.ams.org/amstext-38), Pure and Applied Undergraduate Texts 38, American Mathematical Society, 2019.