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

Showing changes from revision #1 to #2: 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

Using the type of subsets in a universe

a term $\beta_L:\mathcal{T}_\mathcal{U}(L)$

a term $\beta_R:\mathcal{T}_\mathcal{U}(R)$

a term

Given a type $T$ with a dense strict order $\lt$ and 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$ , let us define the following propositions:

{κ DownwardsCloser}_{L 𝒰} : (L) ≔ \prod_{a : 𝒯_{𝒰} (L)} \prod_{b : T} ((b < a) \to \sum_{c : 𝒯_{𝒰} (L)} ι_{L} (c) = b)

~~\kappa_L:~~ 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)

~~a term~~

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}_{R 𝒰} : (\prod_{a : 𝒯_{𝒰} (R)} L, R) ≔ \prod_{a : T} \prod_{b : T} ((a < b) \to \sum_{c : 𝒯_{𝒰} (L)} ι_{L} (c) = a + \sum_{c : 𝒯_{𝒰} (R)} ι_{R} (c) = b)

~~\kappa_R:~~ Locator_\mathcal{U}(L, ~~\prod_{a:\mathcal{T}_\mathcal{U}(R)}~~ 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))

~~a term~~

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}_{L 𝒰} : (\prod_{a : 𝒯_{𝒰} (L)} L \sum_{b : 𝒯_{𝒰} (L)}, a R <) b ≔ {DownwardsOpener}_{𝒰} (L) \times {UpwardsOpener}_{𝒰} (R)

~~\omega_L:~~ Opener_\mathcal{U}(L, ~~\prod_{a:\mathcal{T}_\mathcal{U}(L)}~~ R) ~~\sum_{b:\mathcal{T}_\mathcal{U}(L)}~~ \coloneqq a DownwardsOpener_\mathcal{U}(L) ~~\lt~~ \times b UpwardsOpener_\mathcal{U}(R)

~~a term~~

Using sigma-frames

~~$\omega_R: \prod_{a:\mathcal{T}_\mathcal{U}(R)} \sum_{b:\mathcal{T}_\mathcal{U}(R)} b \lt a$~~

…

~~a term~~

Type of Dedekind cut structures

~~$\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)$~~

The type of Dedekind cut structures on $(L, R)$ is defined as

~~a term~~

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)

~~$\tau_L: \prod_{a:\mathcal{T}_\mathcal{U}(L)} \prod_{b:\mathcal{T}_\mathcal{U}(R)} (i_L(a) \lt i_L(b))$~~

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]$ .

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

Defintion

Using the type of subsets in a universe

Using sigma-frames

Type of Dedekind cut structures

See also