## Defintion ## Wherever you see an order proposition, replace with a open interval. Whenever you see an existential quantifier with an order proposition, replace with a lower/upper unbounded open interval. This should result in actual structure as (dependent) functions between sets for all 8 properties. ### 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: $$Inhabitor_\mathcal{U}(P) \coloneqq \mathcal{T}_\mathcal{U}(P)$$ $$DownwardsCloser_\mathcal{U}(P) \coloneqq \prod_{a:\mathcal{T}_\mathcal{U}(P)} \prod_{b:T} \left((b \lt a) \to fiber(\iota_P,b)\right)$$ $$UpwardsCloser_\mathcal{U}(P) \coloneqq \prod_{a:\mathcal{T}_\mathcal{U}(P)} \prod_{b:T} \left((a \lt b) \to fiber(\iota_P,b)\right)$$ $$DownwardsOpener_\mathcal{U}(P) \coloneqq \prod_{a:\mathcal{T}_\mathcal{U}(P)} \sum_{b:\mathcal{T}_\mathcal{U}(P)} a \lt b$$ $$UpwardsOpener_\mathcal{U}(P) \coloneqq \prod_{a:\mathcal{T}_\mathcal{U}(P)} \sum_{b:\mathcal{T}_\mathcal{U}(P)} b \lt a$$ 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: $$Locator_\mathcal{U}(L, R) \coloneqq \prod_{a:T} \prod_{b:T} \left((a \lt b) \to (fiber(\iota_L,A) + fiber(\iota_R,b))\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))$$ $$Bounder_\mathcal{U}(L, R) \coloneqq Inhabitor_\mathcal{U}(L) \times Inhabitor_\mathcal{U}(R)$$ $$Rounder_\mathcal{U}(L, R) \coloneqq DownwardsCloser_\mathcal{U}(L) \times UpwardsCloser_\mathcal{U}(R)$$ $$Opener_\mathcal{U}(L, R) \coloneqq DownwardsOpener_\mathcal{U}(L) \times UpwardsOpener_\mathcal{U}(R)$$ The type of **$\mathcal{U}$-Dedekind cut structures** on $(L, R)$ is defined as $$DedekindCutStructure_\mathcal{U}(L, R) \coloneqq Bounder_\mathcal{U}(L, R) \times Rounder_\mathcal{U}(L, R) \times Opener_\mathcal{U}(L, R) \times Locator_\mathcal{U}(L, R) \times isTransitive_\mathcal{U}(L, R)$$ A $\mathcal{U}$-Dedekind cut structure on $(L, R)$ is simply a term $\Delta:DedekindCutStructure_\mathcal{U}(L, R)$. $(L, R)$ is said to have a $\mathcal{U}$-Dedekind cut structure if there is a term $\delta:\left[DedekindCutStructure_\mathcal{U}(L, R)\right]$. ### 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 types: $$Inhabitor_\Sigma(P) \coloneqq fiber(P,\top)$$ $$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:Tfiber(P,\top)} \prod_{b:T} (a \lt b) \to (P(b) = \top)$$ $$DownwardsOpener_\Sigma(P) \coloneqq \prod_{a:fiber(P,\top)} \sum_{b:fiber(P,\top)} (a \lt b)$$ $$UpwardsOpener_\Sigma(P) \coloneqq \prod_{a:fiber(P,\top)} \sum_{b:fiber(P,\top)} (b \lt a)$$ 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 types: $$Locator_\Sigma(L, R) \coloneqq \prod_{a:T} \prod_{b:T} \left((a \lt b) \to ((L(a) = \top) + (R(b) = \top))\right)$$ $$isTransitive_\Sigma(L, R) \coloneqq \prod_{a:fiber(L,\top)} \prod_{b:fiber(R,\top)} (a \lt b)$$ $$Bounder_\Sigma(L, R) \coloneqq Inhabitor_\Sigma(L) \times Inhabitor_\Sigma(R)$$ $$isRounded_\Sigma(L, R) \coloneqq isDownwardsClosed_\Sigma(L) \times isUpwardsClosed_\Sigma(R)$$ $$Opener_\Sigma(L, R) \coloneqq DownwardsOpener_\Sigma(L) \times UpwardsOpener_\Sigma(R)$$ The type of **$\Sigma$-Dedekind cut structures** on $(L, R)$ is defined as $$isDedekindCut_\Sigma(L, R) \coloneqq Bounder_\Sigma(L, R) \times Opener_\Sigma(L, R) \times isRounded_\Sigma(L, R) \times Locator_\Sigma(L, R) \times isTransitive_\Sigma(L, R)$$ A $\Sigma$-Dedekind cut structure on $(L, R)$ is simply a term $\Delta:DedekindCutStructure_\Sigma(L, R)$. $(L, R)$ is said to have a $\Sigma$-Dedekind cut structure if there is a term $\delta:\left[DedekindCutStructure_\Sigma(L, R)\right]$. ## See also ## * [[dense strict order]] * [[Dedekind cut]] * [[Dedekind cut structure real numbers]] ## 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))