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

Showing changes from revision #6 to #7: Added | Removed | Changed

Disambiguation page <Dedekind real numbers

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 a $\sigma$-frame, such as the type of propositions in a universe or Sierpinski space: