# Homotopy Type Theory extended Dedekind cut > history (changes)

Showing changes from revision #2 to #3: Added | Removed | Changed

## Defintion

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:

$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))$
$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)$
$isExtendedDedekindCut_\mathcal{U}(L, R) \coloneqq 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 locally $\mathcal{U}$-small extended Dedekind cut if it comes with a term $\delta:isExtendedDedekindCut_\mathcal{U}(L, R)$.

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

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