Homotopy Type Theory
Dedekind cut > history (Rev #1)
Β Defintion
Given a type with a dense strict order , and a pair of subtypes in a universe with monic functions and , let us define the following propositions:
is a Dedekind cut if it comes with a term .
Β Type of Dedekind cuts
The type of Dedekind cuts of in a universe is defined as
Β See also
Revision on April 21, 2022 at 18:58:01 by
Anonymous?.
See the history of this page for a list of all contributions to it.