Homotopy Type Theory
extended Dedekind cut > history (Rev #3, changes)
Showing changes from revision #2 to #3:
Added | Removed | Changed
Defintion
< Dedekind cut
Given a type with a dense strict order , and given a subtype with monic function , let us define the following propositions:
Given a pair of subtypes in a universe with monic functions and , let us define the following propositions:
is a locally -small extended Dedekind cut if it comes with a term .
The type of locally -small extended Dedekind cuts of in a universe is defined as
See also
Revision on June 14, 2022 at 20:25:02 by
Anonymous?.
See the history of this page for a list of all contributions to it.