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

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 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