Showing changes from revision #1 to #2:
Added | Removed | Changed
Defintion
Using the type of subsets in a universe
Given a type with a dense strict order , and given a subtype with monic function , let us define the following propositions:
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:
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 is a extended -Dedekind cut-small extended Dedekind cuts of if it comes with a term in a universe . is defined as
The type of extended -Dedekind cuts of in a universe is defined as
Using sigma-frames
Given a type with a dense strict order , and a $\sigma$-frame , an open subtype is a function . Given an open subtype , let us define the following propositions:
Given a pair of open subtypes in a universe , let us define the following propositions:
is an extended -Dedekind cut if it comes with a term .
The type of extended -Dedekind cuts of for a -frame is defined as
See also