## 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: * [[Cauchy real numbers (disambiguation)]] * [[Dedekind real numbers]] (disambiguation page) * [[Eudoxus real numbers]] * [[localic real numbers]] (opens are binary relations, type is a [[frame]] and lies in a higher [[universe]] in the hierarchy) and [[sigma-localic real numbers]] (opens are functions into [[Sierpinski space]], type is a [[sigma-frame|$\sigma$-frame]] and lies in the same universe) * [[MacNeille real numbers]] or Dedekind-MacNeille real numbers * [[real unit interval]] based real numbers * [[Euclidean real numbers]] or Escardo-Simpson real numbers * The various types of real numbers defined by Peter Freyd using various definitions of the co-algebraic real unit interval. ## 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)