Homotopy Type Theory Dedekind real numbers (disambiguation) > history (Rev #1)

Disambiguation page

There are many different types which are called Dedekind real numbers in the literature. All of them involve the use of Dedekind cuts? in a dense integral subdomain of the rational numbers in their definition, and they differ based upon which definitions of a Dedekind cut are used. These include:

• two-sided Dedekind real numbers?, which is defined using Dedekind cuts, which are defined using the type of all prepositions in a universe.

• lower Dedekind real numbers?, which is defined using only lower Dedekind cuts.

• upper Dedekind real numbers?, which is defined using only upper Dedekind cuts.

• The following types are defined as above but uses Sierpinski space instead of the type of all prepositions in a universe to define Dedekind cuts:

  • predicative two-sided Dedekind real numbers?
  • predicative lower Dedekind real numbers?
  • predicative upper Dedekind real numbers?

• The following types are defined as above but the Dedekind cuts are structure rather than mere property:

  • two-sided Dedekind cut structure real numbers?
  • lower Dedekind cut structure real numbers?
  • upper Dedekind cut structure real numbers?
  • predicative two-sided Dedekind cut structure real numbers?
  • predicative lower Dedekind cut structure real numbers?
  • predicative upper Dedekind cut structure real numbers?

See also

• real numbers for other types of real numbers

References

HoTT book

• Auke B. Booij, Extensional constructive real analysis via locators, (abs:1805.06781)