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 pair of subtypes in a universe with monic functions and , let us define the following propositions:
The type of -Dedekind cut structures on is defined as
A -Dedekind cut structure on is simply a term .
is said to have a -Dedekind cut structure if there is a term .
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 types:
Given a pair of open subtypes in a universe , let us define the following types:
The type of -Dedekind cut structures on is defined as
A -Dedekind cut structure on is simply a term .
is said to have a -Dedekind cut structure if there is a term .
See also
References