## Defintion ## ### Using the type of subsets in a universe ### 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: $$DownwardsCloser_\mathcal{U}(L) \coloneqq \prod_{a:\mathcal{T}_\mathcal{U}(L)} \prod_{b:T} \left((b \lt a) \to \sum_{c:\mathcal{T}_\mathcal{U}(L)} \iota_L(c) = b\right)$$ $$UpwardsCloser_\mathcal{U}(R) \coloneqq \prod_{a:\mathcal{T}_\mathcal{U}(R)} \prod_{b:T} \left((a \lt b) \to \sum_{c:\mathcal{T}_\mathcal{U}(R)} \iota_R(c) = b\right)$$ $$DownwardsOpener_\mathcal{U}(L) \coloneqq \prod_{a:\mathcal{T}_\mathcal{U}(L)} \sum_{b:\mathcal{T}_\mathcal{U}(L)} a \lt b$$ $$UpwardsOpener_\mathcal{U}(R) \coloneqq \prod_{a:\mathcal{T}_\mathcal{U}(R)} \sum_{b:\mathcal{T}_\mathcal{U}(R)} b \lt a$$ $$Locator_\mathcal{U}(L, R) \coloneqq \prod_{a:T} \prod_{b:T} \left((a \lt b) \to \sum_{c:\mathcal{T}_\mathcal{U}(L)} \iota_L(c) = a + \sum_{c:\mathcal{T}_\mathcal{U}(R)} \iota_R(c) = 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 \mathcal{T}_\mathcal{U}(L) \times \mathcal{T}_\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)$$ ### Using sigma-frames ### ... ### Type of Dedekind cut structures ### The type of **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 Dedekind cut structure on $(L, R)$ is simply a term $\Delta:DedekindCutStructure_\mathcal{U}(L, R)$. $(L, R)$ is said to have a Dedekind cut structure if there is a term $\delta:\left[DedekindCutStructure_\mathcal{U}(L, R)\right]$. ## See also ## * [[dense strict order]] * [[Dedekind cut]] * [[strict order with Dedekind cut structure]]