Homotopy Type Theory Dedekind cut (disambiguation) > history (Rev #2)

Disambiguation page

There are many different terms which are called Dedekind cuts in the literature.

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

  • two-sided bounded Dedekind cut?
  • lower bounded Dedekind cut?
  • upper bounded Dedekind cut?
  • two-sided unbounded Dedekind cut?
  • lower unbounded Dedekind cut?
  • upper unbounded Dedekind cut?
  • two-sided bounded Dedekind cut structure?
  • lower bounded Dedekind cut structure?
  • upper bounded Dedekind cut structure?
  • two-sided unbounded Dedekind cut structure?
  • lower unbounded Dedekind cut structure?
  • upper unbounded Dedekind cut structure?

The following terms 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 type of Dedekind cuts form a $\sigma$-frame in the same universe rather than a large frame in the next universe in the hierarchy.

  • two-sided bounded sigma-Dedekind cut?
  • lower bounded sigma-Dedekind cut?
  • upper bounded sigma-Dedekind cut?
  • two-sided unbounded sigma-Dedekind cut?
  • lower unbounded sigma-Dedekind cut?
  • upper unbounded sigma-Dedekind cut?
  • two-sided bounded sigma-Dedekind cut structure?
  • lower bounded sigma-Dedekind cut structure?
  • upper bounded sigma-Dedekind cut structure?
  • two-sided unbounded sigma-Dedekind cut structure?
  • lower unbounded sigma-Dedekind cut structure?
  • upper unbounded sigma-Dedekind cut structure?

See also

References

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