# Homotopy Type Theory Dedekind cut > history (changes)

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

## Β Defintion

### 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:

$isInhabited_\mathcal{U}(P) \coloneqq \left[\mathcal{T}_\mathcal{U}(P)\right]$
$isDownwardsClosed_\mathcal{U}(P) \coloneqq \prod_{a:\mathcal{T}_\mathcal{U}(P)} \prod_{b:T} \left((b \lt a) \to \left[fiber(\iota_P,b)\right]\right)$
$isUpwardsClosed_\mathcal{U}(P) \coloneqq \prod_{a:\mathcal{T}_\mathcal{U}(P)} \prod_{b:T} \left((a \lt b) \to \left[\fiber(\iota_P,b)\right]\right)$
$isDownwardsOpen_\mathcal{U}(P) \coloneqq \prod_{a:\mathcal{T}_\mathcal{U}(P)} \left[\sum_{b:\mathcal{T}_\mathcal{U}(P)} a \lt b\right]$
$isUpwardsOpen_\mathcal{U}(P) \coloneqq \prod_{a:\mathcal{T}_\mathcal{U}(P)} \left[\sum_{b:\mathcal{T}_\mathcal{U}(P)} b \lt a\right]$

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:

$isLocated_\mathcal{U}(L, R) \coloneqq \prod_{a:T} \prod_{b:T} \left((a \lt b) \to \left[fiber(\iota_L,a) + fiber(\iota_R,b)\right]\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))$
$isBounded_\mathcal{U}(L, R) \coloneqq isInhabited_\mathcal{U}(L) \times isInhabited_\mathcal{U}(R)$
$isOpen_\mathcal{U}(L, R) \coloneqq isDownwardsOpen_\mathcal{U}(L) \times isUpwardsOpen_\mathcal{U}(R)$
$isRounded_\mathcal{U}(L, R) \coloneqq isDownwardsClosed_\mathcal{U}(L) \times isUpwardsClosed_\mathcal{U}(R)$
$isDedekindCut_\mathcal{U}(L, R) \coloneqq isBounded_\mathcal{U}(L, R) \times isOpen_\mathcal{U}(L, R) \times isRounded_\mathcal{U}(L, R) \times isLocated_\mathcal{U}(L, R) \times isTransitive_\mathcal{U}(L, R)$

$(L, R)$ is a $\mathcal{U}$-Dedekind cut if it comes with a term $\delta:isDedekindCut_\mathcal{U}(L, R)$.

The type of $\mathcal{U}$-Dedekind cuts of $T$ in a universe $\mathcal{U}$ is defined as

$DedekindCut_\mathcal{U}(T) \coloneqq \sum_{(L, R):Sub_\mathcal{U}(T) \times Sub_\mathcal{U}(T)} isDedekindCut_\mathcal{U}(L, R)$

### Using open intervals

Given a type $T$ with a dense strict order $\lt$, let us define the family of lower bounded open intervals $a:T \vdash (a,\infty)$ and upper bounded open intervals $a:T \vdash (-\infty, a)$. The type of $\mathcal{U}$-Dedekind cuts in a universe $\mathcal{U}$ is a frame generated by $(a,\infty)$ and $(-\infty, a)$ such that

$T \subseteq \bigcup_{a:T}^\mathcal{U} (a,\infty)$
$T \subseteq \bigcup_{a:T}^\mathcal{U} (-\infty,a)$
$\prod_{a:T} \prod_{b:T} (a \lt b) \to ((b,\infty) \subseteq (a,\infty))$
$\prod_{a:T} \prod_{b:T} (b \lt a) \to ((-\infty,b) \subseteq (-\infty,a))$
$\prod_{a:T} (a,\infty) \subseteq \bigcup_{b:(a,\infty)}^\mathcal{U} (b,\infty)$
$\prod_{a:T} (-\infty,a) \subseteq \bigcup_{b:(-\infty,a)}^\mathcal{U} (-\infty,b)$
$\prod_{a:T} \prod_{b:T} (a \lt b) \to T \subseteq (a, \infty) \cup (-\infty, b)$
$\prod_{a:T} \prod_{b:T} (a,\infty) \cap (-\infty,b) \subseteq (a,b)$

A $\mathcal{U}$-Dedekind cut is an element of this frame.

### 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 propositions:

$isInhabited_\Sigma(P) \coloneqq \left[fiber(P,\top)\right]$
$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:fiber(P,\top)} \prod_{b:T} (a \lt b) \to (P(b) = \top)$
$isDownwardsOpen_\Sigma(P) \coloneqq \prod_{a:fiber(P,\top)} \to \left[\sum_{b:fiber(P,\top)} (a \lt b)\right]$
$isUpwardsOpen_\Sigma(P) \coloneqq \prod_{a:fiber(P,\top)} \to \left[\sum_{b:fiber(P,\top)} (b \lt a)\right]$

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 propositions:

$isLocated_\Sigma(L, R) \coloneqq \prod_{a:T} \prod_{b:T} \left((a \lt b) \to \left[(L(a) = \top) + (R(b) = \top)\right]\right)$
$isTransitive_\Sigma(L, R) \coloneqq \prod_{a:fiber(L,\top)} \prod_{b:fiber(R,\top)} (a \lt b)$
$isBounded_\Sigma(L, R) \coloneqq isInhabited_\Sigma(L) \times isInhabited_\Sigma(R)$
$isOpen_\Sigma(L, R) \coloneqq isDownwardsOpen_\Sigma(L) \times isUpwardsOpen_\Sigma(R)$
$isRounded_\Sigma(L, R) \coloneqq isDownwardsClosed_\Sigma(L) \times isUpwardsClosed_\Sigma(R)$
$isDedekindCut_\Sigma(L, R) \coloneqq isBounded_\Sigma(L, R) \times isOpen_\Sigma(L, R) \times isRounded_\Sigma(L, R) \times isLocated_\Sigma(L, R) \times isTransitive_\Sigma(L, R)$

$(L, R)$ is a $\Sigma$-Dedekind cut if it comes with a term $\delta:isDedekindCut_\Sigma(L, R)$.

The type of $\Sigma$-Dedekind cuts of $T$ for a $\sigma$-frame $\Sigma$ is defined as

$DedekindCut_\Sigma(T) \coloneqq \sum_{(L, R):(T \to \Sigma) \times (T \to \Sigma)} isDedekindCut_\Sigma(L, R)$