Homotopy Type Theory Dedekind real numbers (disambiguation) > history (Rev #3, changes)

Showing changes from revision #2 to #3: Added | Removed | Changed

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.

The following real number types are defined using the type of all propositions in a universe, so that the real number types form a (large) frame (in the next universe in the hierarchy):

  • two-sided Dedekind real number?
  • lower Dedekind real number?
  • upper Dedekind real number?
  • two-sided extended Dedekind real number?
  • lower extended Dedekind real number?
  • upper extended Dedekind real number?
  • two-sided Dedekind cut structure real number?
  • lower Dedekind cut structure real number?
  • upper Dedekind cut structure real number?
  • two-sided extended Dedekind cut structure real number?
  • lower extended Dedekind cut structure real number?
  • upper extended Dedekind cut structure real number?

The following real number types are defined as above but uses Sierpinski space instead of the type of all prepositions in a universe to define Dedekind cuts, so that the real number types form a $\sigma$-frame in the same universe rather than a large frame in the next universe in the hierarchy.

  • two-sided sigma-Dedekind real number?
  • lower sigma-Dedekind real number?
  • upper sigma-Dedekind real number?
  • two-sided extended sigma-Dedekind real number?
  • lower extended sigma-Dedekind real number?
  • upper extended sigma-Dedekind real number?
  • two-sided sigma-Dedekind cut structure real number?
  • lower sigma-Dedekind cut structure real number?
  • upper sigma-Dedekind cut structure real number?
  • two-sided extended sigma-Dedekind cut structure real number?
  • lower extended sigma-Dedekind cut structure real number?
  • upper extended sigma-Dedekind cut structure real number?

See also

References

HoTT book

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

Revision on March 12, 2022 at 05:53:10 by Anonymous?. See the history of this page for a list of all contributions to it.