Homotopy Type Theory Dedekind cut structure > history (Rev #1, changes)

Showing changes from revision #0 to #1: Added | ~~Removed~~ | ~~Chan~~ged

Defintion

Given a type $T$ with a dense strict order $\lt$ , a Dedekind cut structure is a pair of subtypes $(L, R):Sub_\mathcal{U}(T) \times Sub_\mathcal{U}(T)$ in a universe $\mathcal{U}$ with monic functions $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))

Homotopy Type Theory Dedekind cut structure > history (Rev #1, changes)

Defintion

See also