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

Showing changes from revision #1 to #2: 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:

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)$
 isDownwardsClosed_\mathcal{U}(P) isDownwardsOpen_\mathcal{U}(P) \coloneqq \prod_{a:\mathcal{T}_\mathcal{U}(P)} \prod_{b:T} \left[\sum_{b:\mathcal{T}_\mathcal{U}(P)} \left((b a \lt a) b\right] \to \left[fiber(\iota_P,b)\right]\right)
 isUpwardsClosed_\mathcal{U}(P) isUpwardsOpen_\mathcal{U}(P) \coloneqq \prod_{a:\mathcal{T}_\mathcal{U}(P)} \prod_{b:T} \left[\sum_{b:\mathcal{T}_\mathcal{U}(P)} \left((a b \lt b) a\right] \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:

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

$(L, R)$The type of locally is a $\mathcal{U}$extended $\mathcal{U}$-Dedekind cut-small extended Dedekind cuts of if it comes with a term $T$$\delta:isExtendedDedekindCut_\mathcal{U}(L, R)$ in a universe .$\mathcal{U}$ is defined as

The type of extended $\mathcal{U}$-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)$
$ExtendedDedekindCut_\mathcal{U}(T) \coloneqq \sum_{(L, R):Sub_\mathcal{U}(T) \times Sub_\mathcal{U}(T)} isExtendedDedekindCut_\mathcal{U}(L, R)$

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

$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)$
$isOpen_\Sigma(L, R) \coloneqq isDownwardsOpen_\Sigma(L) \times isUpwardsOpen_\Sigma(R)$
$isRounded_\Sigma(L, R) \coloneqq isDownwardsClosed_\Sigma(L) \times isUpwardsClosed_\Sigma(R)$
$isExtendedDedekindCut_\Sigma(L, R) \coloneqq isOpen_\Sigma(L, R) \times isRounded_\Sigma(L, R) \times isLocated_\Sigma(L, R) \times isTransitive_\Sigma(L, R)$

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

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

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