## Definition ## The type of __real numbers__ $\mathbb{R}$ is defined as the terminal [[Archimedean ordered field]] or the terminal [[Archimedean ordered integral domain]]. ## Other types called 'real numbers' ## There are many other different types which are called real numbers in the literature, many of which are not the same as the real numbers defined above. These include: * [[Cauchy real numbers (disambiguation)]] * [[Dedekind real numbers]] (disambiguation page) * [[Eudoxus real numbers]] * [[localic real numbers]] (forms a [[frame]] and lies in a higher [[universe]] in the hierarchy) and [[sigma-localic real numbers]] (forms 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 ## [[HoTT book]]