Showing changes from revision #6 to #7:
Added | Removed | Changed
The type of real numbers is defined a as the terminallocally (-1)-connected? Hausdorff sober? Archimedean ordered field or with the a terminalArchimedean ordered integral domaincompact? real unit interval? .
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 numbers. defined above. These include:
Dedekind real numbers (disambiguation page)
localic real numbers? (forms (opens are binary relations, type is aframe and lies in a higher universe in the hierarchy) and sigma-localic real numbers? (forms (opens a are functions intoSierpinski space, type is 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.
Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)
Andrej Bauer and Paul Taylor, The Dedekind Reals in Abstract Stone Duality