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

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 Dedekind cut?
  • lower Dedekind cut?
  • upper Dedekind cut?
  • two-sided unbounded Dedekind cut?
  • lower unbounded Dedekind cut?
  • upper unbounded Dedekind cut?
  • two-sided Dedekind cut structure?
  • lower Dedekind cut structure?
  • upper 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 sigma-Dedekind cut?
  • lower sigma-Dedekind cut?
  • upper sigma-Dedekind cut?
  • two-sided unbounded sigma-Dedekind cut?
  • lower unbounded sigma-Dedekind cut?
  • upper unbounded sigma-Dedekind cut?
  • two-sided sigma-Dedekind cut structure?
  • lower sigma-Dedekind cut structure?
  • upper 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 03:10:43 by Anonymous?. See the history of this page for a list of all contributions to it.