## Defintion ## Given a type $T$ with a [[dense strict order]] $\lt$, a **Dedekind cut structure** is 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$ with * a term $\beta_L:\mathcal{T}_\mathcal{U}(L)$ * a term $\beta_R:\mathcal{T}_\mathcal{U}(R)$ * a term $$\kappa_L: \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)$$ * a term $$\kappa_R: \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)$$ * a term $$\omega_L: \prod_{a:\mathcal{T}_\mathcal{U}(L)} \sum_{b:\mathcal{T}_\mathcal{U}(L)} a \lt b$$ * a term $$\omega_R: \prod_{a:\mathcal{T}_\mathcal{U}(R)} \sum_{b:\mathcal{T}_\mathcal{U}(R)} b \lt a$$ * a term $$\lambda_L: \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)$$ * a term $$\tau_L: \prod_{a:\mathcal{T}_\mathcal{U}(L)} \prod_{b:\mathcal{T}_\mathcal{U}(R)} (i_L(a) \lt i_L(b))$$ ## See also ## * [[dense strict order]] * [[Dedekind cut]] * [[strict order with Dedekind cut structure]]