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

Showing changes from revision #3 to #4: 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 cut cuts s 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 $\sigma$-frame , (in such as the next type of propositions in a universe or universe Sierpinski space : in the hierarchy):

  • two-sided Dedekind real number?Dedekind real numbers
  • lower Dedekind real number?Dedekind cut structure real numbers
  • 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

Revision on April 14, 2022 at 02:32:14 by Anonymous?. See the history of this page for a list of all contributions to it.