Β 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:
is a -Dedekind cut if it comes with a term .
The type of -Dedekind cuts of in a universe is defined as
Using open intervals
Given a type with a dense strict order , let us define the family of lower bounded open intervals and upper bounded open intervals . The type of -Dedekind cuts in a universe is a frame generated by and such that
A -Dedekind cut is an element of this frame.
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 a -Dedekind cut if it comes with a term .
The type of -Dedekind cuts of for a -frame is defined as
Β See also
References