# Homotopy Type Theory Dedekind cut structure > history (Rev #5, changes)

Showing changes from revision #4 to #5: Added | Removed | Changed

## Defintion

Wherever you see an order proposition, replace with a open interval. Whenever you see an existential quantifier with an order proposition, replace with a lower/upper unbounded open interval. This should result in actual structure as (dependent) functions between sets for all 8 properties.

### Using the type of subsets in a universe

Given a type $T$ with a dense strict order $\lt$, and given a subtype $P:Sub_\mathcal{U}(T)$ with monic function $i_P:\mathcal{T}_\mathcal{U}(P) \to T$, let us define the following propositions:

$Inhabitor_\mathcal{U}(P) \coloneqq \mathcal{T}_\mathcal{U}(P)$
$DownwardsCloser_\mathcal{U}(P) \coloneqq \prod_{a:\mathcal{T}_\mathcal{U}(P)} \prod_{b:T} \left((b \lt a) \to fiber(\iota_P,b)\right)$
$UpwardsCloser_\mathcal{U}(P) \coloneqq \prod_{a:\mathcal{T}_\mathcal{U}(P)} \prod_{b:T} \left((a \lt b) \to fiber(\iota_P,b)\right)$
$DownwardsOpener_\mathcal{U}(P) \coloneqq \prod_{a:\mathcal{T}_\mathcal{U}(P)} \sum_{b:\mathcal{T}_\mathcal{U}(P)} a \lt b$
$UpwardsOpener_\mathcal{U}(P) \coloneqq \prod_{a:\mathcal{T}_\mathcal{U}(P)} \sum_{b:\mathcal{T}_\mathcal{U}(P)} b \lt a$

Given a pair of subtypes $(L, R):Sub_\mathcal{U}(T) \times Sub_\mathcal{U}(T)$ in a universe $\mathcal{U}$ with monic functions $i_L:\mathcal{T}_\mathcal{U}(L) \to T$ and $i_R:\mathcal{T}_\mathcal{U}(R) \to T$, let us define the following propositions:

$Locator_\mathcal{U}(L, R) \coloneqq \prod_{a:T} \prod_{b:T} \left((a \lt b) \to (fiber(\iota_L,A) + fiber(\iota_R,b))\right)$
$isTransitive_\mathcal{U}(L, R) \coloneqq \prod_{a:\mathcal{T}_\mathcal{U}(L)} \prod_{b:\mathcal{T}_\mathcal{U}(R)} (i_L(a) \lt i_L(b))$
$Bounder_\mathcal{U}(L, R) \coloneqq Inhabitor_\mathcal{U}(L) \times Inhabitor_\mathcal{U}(R)$
$Rounder_\mathcal{U}(L, R) \coloneqq DownwardsCloser_\mathcal{U}(L) \times UpwardsCloser_\mathcal{U}(R)$
$Opener_\mathcal{U}(L, R) \coloneqq DownwardsOpener_\mathcal{U}(L) \times UpwardsOpener_\mathcal{U}(R)$

The type of $\mathcal{U}$-Dedekind cut structures on $(L, R)$ is defined as

$DedekindCutStructure_\mathcal{U}(L, R) \coloneqq Bounder_\mathcal{U}(L, R) \times Rounder_\mathcal{U}(L, R) \times Opener_\mathcal{U}(L, R) \times Locator_\mathcal{U}(L, R) \times isTransitive_\mathcal{U}(L, R)$

A $\mathcal{U}$-Dedekind cut structure on $(L, R)$ is simply a term $\Delta:DedekindCutStructure_\mathcal{U}(L, R)$.

$(L, R)$ is said to have a $\mathcal{U}$-Dedekind cut structure if there is a term $\delta:\left[DedekindCutStructure_\mathcal{U}(L, R)\right]$.

### Using sigma-frames

Given a type $T$ with a dense strict order $\lt$, and a $\sigma$-frame $\Sigma$, an open subtype is a function $P:T \to \Sigma$. Given an open subtype $P:T \to \Sigma$, let us define the following types:

$Inhabitor_\Sigma(P) \coloneqq fiber(P,\top)$
$isDownwardsClosed_\Sigma(P) \coloneqq \prod_{a:fiber(P,\top)} \prod_{b:T} (b \lt a) \to (P(b) = \top)$
$isUpwardsClosed_\Sigma(P) \coloneqq \prod_{a:Tfiber(P,\top)} \prod_{b:T} (a \lt b) \to (P(b) = \top)$
$DownwardsOpener_\Sigma(P) \coloneqq \prod_{a:fiber(P,\top)} \sum_{b:fiber(P,\top)} (a \lt b)$
$UpwardsOpener_\Sigma(P) \coloneqq \prod_{a:fiber(P,\top)} \sum_{b:fiber(P,\top)} (b \lt a)$

Given a pair of open subtypes $(L, R):(T \to \Sigma) \times (T \to \Sigma)$ in a universe $\mathcal{U}$, let us define the following types:

$Locator_\Sigma(L, R) \coloneqq \prod_{a:T} \prod_{b:T} \left((a \lt b) \to ((L(a) = \top) + (R(b) = \top))\right)$
$isTransitive_\Sigma(L, R) \coloneqq \prod_{a:fiber(L,\top)} \prod_{b:fiber(R,\top)} (a \lt b)$
$Bounder_\Sigma(L, R) \coloneqq Inhabitor_\Sigma(L) \times Inhabitor_\Sigma(R)$
$isRounded_\Sigma(L, R) \coloneqq isDownwardsClosed_\Sigma(L) \times isUpwardsClosed_\Sigma(R)$
$Opener_\Sigma(L, R) \coloneqq DownwardsOpener_\Sigma(L) \times UpwardsOpener_\Sigma(R)$

The type of $\Sigma$-Dedekind cut structures on $(L, R)$ is defined as

$isDedekindCut_\Sigma(L, R) \coloneqq Bounder_\Sigma(L, R) \times Opener_\Sigma(L, R) \times isRounded_\Sigma(L, R) \times Locator_\Sigma(L, R) \times isTransitive_\Sigma(L, R)$

A $\Sigma$-Dedekind cut structure on $(L, R)$ is simply a term $\Delta:DedekindCutStructure_\Sigma(L, R)$.

$(L, R)$ is said to have a $\Sigma$-Dedekind cut structure if there is a term $\delta:\left[DedekindCutStructure_\Sigma(L, R)\right]$.