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

Defintion

Using the type of subsets in a universe

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

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

Defintion

Using the type of subsets in a universe

Using sigma-frames

Type of Dedekind cut structures

See also