## 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 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: $$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 sigma-frames ### Given a type $T$ with a [[dense strict order]] $\lt$, and a [[sigma-frame|$\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 [[proposition]]s: $$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)$$ ## See also ## * [[dense strict order]] * [[Dedekind cut structure]] * [[Dedekind real numbers]] * [[locale of open intervals]] ## References ## * Univalent Foundations Project, [[HoTT book|Homotopy Type Theory – Univalent Foundations of Mathematics]] (2013) * Auke B. Booij, Extensional constructive real analysis via locators, ([abs:1805.06781](https://arxiv.org/abs/1805.06781))