## Defintion ## Given a type $T$ with a [[dense strict order]] $\lt$, and a pair of [[subtype]]s $(L, R):Sub_\mathcal{U}(T) \times Sub_\mathcal{U}(T)$ in a universe $\mathcal{U}$ with [[monic function]]s $i_L:\mathcal{T}_\mathcal{U}(L) \to T$ and $i_R:\mathcal{T}_\mathcal{U}(R) \to T$, let us define the following [[proposition]]s: $$isInhabited_\mathcal{U}(L) \coloneqq \left[\mathcal{T}_\mathcal{U}(L)\right]$$ $$isInhabited_\mathcal{U}(R) \coloneqq \beta_R:\left[\mathcal{T}_\mathcal{U}(R)\right]$$ $$isDownwardsClosed_\mathcal{U}(L) \coloneqq \prod_{a:\mathcal{T}_\mathcal{U}(L)} \prod_{b:T} \left((b \lt a) \to \left[\sum_{c:\mathcal{T}_\mathcal{U}(L)} \iota_L(c) = b\right]\right)$$ $$isUpwardsClosed_\mathcal{U}(R) \coloneqq \prod_{a:\mathcal{T}_\mathcal{U}(R)} \prod_{b:T} \left((a \lt b) \to \left[\sum_{c:\mathcal{T}_\mathcal{U}(R)} \iota_R(c) = b\right]\right)$$ $$isDownwardsOpen_\mathcal{U}(L) \coloneqq \prod_{a:\mathcal{T}_\mathcal{U}(L)} \left[\sum_{b:\mathcal{T}_\mathcal{U}(L)} a \lt b\right]$$ $$isUpwardsOpen_\mathcal{U}(R) \coloneqq \prod_{a:\mathcal{T}_\mathcal{U}(R)} \left[\sum_{b:\mathcal{T}_\mathcal{U}(R)} b \lt a\right]$$ $$isLocated_\mathcal{U}(L, R) \coloneqq \prod_{a:T} \prod_{b:T} \left((a \lt b) \to \left[\left[\sum_{c:\mathcal{T}_\mathcal{U}(L)} \iota_L(c) = a\right] + \left[\sum_{c:\mathcal{T}_\mathcal{U}(R)} \iota_R(c) = b\right]\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 **Dedekind cut** if it comes with a term $\delta:isDedekindCut_\mathcal{U}(L, R)$. ## Type of Dedekind cuts ## The type of 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)$$ ## See also ## * [[dense strict order]] * [[Dedekind complete dense strict order]] * [[Dedekind cut structure]] * [[Dedekind real numbers]] * [[locale of open intervals]]