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

Showing changes from revision #2 to #3: Added | ~~Removed~~ | ~~Chan~~ged

Defintion

Using the type of subsets in a universe

Given a type $T$ with a dense strict order $\lt$ , and given a ~~pair~~ ofsubtype s $(P L, R) : {Sub}_{𝒰} (T) \times {Sub}_{𝒰} (T)$ ~~(L,~~ P:Sub_\mathcal{U}(T) ~~R):Sub_\mathcal{U}(T)~~ ~~\times~~ ~~Sub_\mathcal{U}(T)~~ in with a ~~universe~~ ~~$\mathcal{U}$~~ ~~with~~ monic function s $i_{L P} : 𝒯_{𝒰} (L P) \to T$ ~~i_L:\mathcal{T}_\mathcal{U}(L)~~ i_P:\mathcal{T}_\mathcal{U}(P) \to T , ~~and~~ let us define the following propositions: ~~$i_R:\mathcal{T}_\mathcal{U}(R) \to T$~~ ~~, let us define the following~~ ~~proposition~~s:

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

~~DownwardsCloser_\mathcal{U}(L)~~ Inhabitor_\mathcal{U}(P) \coloneqq ~~\prod_{a:\mathcal{T}_\mathcal{U}(L)}~~ \mathcal{T}_\mathcal{U}(P) ~~\prod_{b:T}~~ ~~\left((b~~ ~~\lt~~ a) ~~\to~~ ~~\sum_{c:\mathcal{T}_\mathcal{U}(L)}~~ ~~\iota_L(c)~~ = ~~b\right)~~

{UpwardsCloser DownwardsCloser}_{𝒰} (R P) ≔ \prod_{a : 𝒯_{𝒰} (R P)} \prod_{b : T} ((a < b < a) \to \sum_{c : 𝒯_{𝒰} (R)} fiber ι_{R} (c ι_{P}), = b))

~~UpwardsCloser_\mathcal{U}(R)~~ DownwardsCloser_\mathcal{U}(P) \coloneqq ~~\prod_{a:\mathcal{T}_\mathcal{U}(R)}~~ \prod_{a:\mathcal{T}_\mathcal{U}(P)} \prod_{b:T} ~~\left((a~~ \left((b \lt b) a) \to ~~\sum_{c:\mathcal{T}_\mathcal{U}(R)}~~ fiber(\iota_P,b)\right) ~~\iota_R(c)~~ = ~~b\right)~~

{DownwardsOpener UpwardsCloser}_{𝒰} (L P) ≔ \prod_{a : 𝒯_{𝒰} (L P)} \underset{b : 𝒯_{𝒰} T (L)}{\sum \prod} a ((a < b) \to fiber (ι_{P}, b)) < b

~~DownwardsOpener_\mathcal{U}(L)~~ UpwardsCloser_\mathcal{U}(P) \coloneqq ~~\prod_{a:\mathcal{T}_\mathcal{U}(L)}~~ \prod_{a:\mathcal{T}_\mathcal{U}(P)} ~~\sum_{b:\mathcal{T}_\mathcal{U}(L)}~~ \prod_{b:T} a \left((a \lt b b) \to fiber(\iota_P,b)\right)

{UpwardsOpener DownwardsOpener}_{𝒰} (R P) ≔ \prod_{a : 𝒯_{𝒰} (R P)} \sum_{b : 𝒯_{𝒰} (R P)} b < a < b

~~UpwardsOpener_\mathcal{U}(R)~~ DownwardsOpener_\mathcal{U}(P) \coloneqq ~~\prod_{a:\mathcal{T}_\mathcal{U}(R)}~~ \prod_{a:\mathcal{T}_\mathcal{U}(P)} ~~\sum_{b:\mathcal{T}_\mathcal{U}(R)}~~ \sum_{b:\mathcal{T}_\mathcal{U}(P)} b ~~\lt~~ a \lt b

{Locator UpwardsOpener}_{𝒰} (L P, R) ≔ \prod_{a : T 𝒯_{𝒰} (P)} \underset{b : T 𝒯_{𝒰} (P)}{\prod \sum} ((a < b) \to \sum_{c : 𝒯_{𝒰} (L)} ι_{L} (c) = a + \sum_{c : 𝒯_{𝒰} (R)} ι_{R} (c) = b) b < a

~~Locator_\mathcal{U}(L,~~ UpwardsOpener_\mathcal{U}(P) R) \coloneqq ~~\prod_{a:T}~~ \prod_{a:\mathcal{T}_\mathcal{U}(P)} ~~\prod_{b:T}~~ \sum_{b:\mathcal{T}_\mathcal{U}(P)} ~~\left((a~~ b \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)$~~

Given 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:

~~$Rounder_\mathcal{U}(L, R) \coloneqq DownwardsCloser_\mathcal{U}(L) \times UpwardsCloser_\mathcal{U}(R)$~~

{Opener Locator}_{𝒰} (L, R) ≔ {DownwardsOpener}_{𝒰} \prod_{a : T} (\prod_{b : T} L ((a < b) \to (fiber (ι_{L}, A) + fiber (ι_{R}, b)))) \times {UpwardsOpener}_{𝒰} (R)

~~Opener_\mathcal{U}(L,~~ Locator_\mathcal{U}(L, R) \coloneqq ~~DownwardsOpener_\mathcal{U}(L)~~ \prod_{a:T} ~~\times~~ \prod_{b:T} ~~UpwardsOpener_\mathcal{U}(R)~~ \left((a \lt b) \to (fiber(\iota_L,A) + fiber(\iota_R,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 Inhabitor_\mathcal{U}(L) \times Inhabitor_\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)

The type of $\mathcal{U}$ -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 $\mathcal{U}$ -Dedekind cut structure on $(L, R)$ is simply a term $\Delta:DedekindCutStructure_\mathcal{U}(L, R)$ .

$(L, R)$ is said to have a $\mathcal{U}$ -Dedekind cut structure if there is a term $\delta:\left[DedekindCutStructure_\mathcal{U}(L, R)\right]$ .

Using sigma-frames

… Given a type $T$ with a dense strict order $\lt$ , and a $\sigma$-frame $\Sigma$ , an open subtype is a function $P:T \to \Sigma$ . Given an open subtype $P:T \to \Sigma$ , let us define the following types:

~~Type of Dedekind cut structures~~

Inhabitor_\Sigma(P) \coloneqq fiber(P,\top)

isDownwardsClosed_\Sigma(P) \coloneqq \prod_{a:fiber(P,\top)} \prod_{b:T} (b \lt a) \to (P(b) = \top)

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

isUpwardsClosed_\Sigma(P) \coloneqq \prod_{a:Tfiber(P,\top)} \prod_{b:T} (a \lt b) \to (P(b) = \top)

DownwardsOpener_\Sigma(P) \coloneqq \prod_{a:fiber(P,\top)} \sum_{b:fiber(P,\top)} (a \lt b)

{DedekindCutStructure UpwardsOpener}_{𝒰 Σ} (L P, R) ≔ {Bounder}_{𝒰} \prod_{a : fiber (P, ⊤)} \sum_{b : fiber (P, ⊤)} (L b, < R a) \times {Rounder}_{𝒰} (L, R) \times {Opener}_{𝒰} (L, R) \times {Locator}_{𝒰} (L, R) \times {isTransitive}_{𝒰} (L, R)

~~DedekindCutStructure_\mathcal{U}(L,~~ UpwardsOpener_\Sigma(P) R) \coloneqq ~~Bounder_\mathcal{U}(L,~~ \prod_{a:fiber(P,\top)} R) \sum_{b:fiber(P,\top)} ~~\times~~ (b ~~Rounder_\mathcal{U}(L,~~ \lt R) a) ~~\times~~ ~~Opener_\mathcal{U}(L,~~ R) ~~\times~~ ~~Locator_\mathcal{U}(L,~~ R) ~~\times~~ ~~isTransitive_\mathcal{U}(L,~~ R)

A Given ~~Dedekind~~ a ~~cut~~ pair ~~structure~~ of on open subtypes $(L, R) : (T \to Σ) \times (T \to Σ)$ (L, R) R):(T \to \Sigma) \times (T \to \Sigma) is in ~~simply~~ a ~~term~~ universe $Δ 𝒰 : {DedekindCutStructure}_{𝒰} (L, R)$ ~~\Delta:DedekindCutStructure_\mathcal{U}(L,~~ \mathcal{U} R) . , let us define the following types:

~~$(L, R)$ is said to have a Dedekind cut structure if there is a term $\delta:\left[DedekindCutStructure_\mathcal{U}(L, R)\right]$ .~~

Locator_\Sigma(L, R) \coloneqq \prod_{a:T} \prod_{b:T} \left((a \lt b) \to ((L(a) = \top) + (R(b) = \top))\right)

isTransitive_\Sigma(L, R) \coloneqq \prod_{a:fiber(L,\top)} \prod_{b:fiber(R,\top)} (a \lt b)

Bounder_\Sigma(L, R) \coloneqq Inhabitor_\Sigma(L) \times Inhabitor_\Sigma(R)

isRounded_\Sigma(L, R) \coloneqq isDownwardsClosed_\Sigma(L) \times isUpwardsClosed_\Sigma(R)

Opener_\Sigma(L, R) \coloneqq DownwardsOpener_\Sigma(L) \times UpwardsOpener_\Sigma(R)

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

isDedekindCut_\Sigma(L, R) \coloneqq Bounder_\Sigma(L, R) \times Opener_\Sigma(L, R) \times isRounded_\Sigma(L, R) \times Locator_\Sigma(L, R) \times isTransitive_\Sigma(L, R)

A $\Sigma$ -Dedekind cut structure on $(L, R)$ is simply a term $\Delta:DedekindCutStructure_\Sigma(L, R)$ .

$(L, R)$ is said to have a $\Sigma$ -Dedekind cut structure if there is a term $\delta:\left[DedekindCutStructure_\Sigma(L, R)\right]$ .

References

Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)
Auke B. Booij, Extensional constructive real analysis via locators, (abs:1805.06781)

Revision on April 21, 2022 at 21:12:55 by Anonymous?. See the history of this page for a list of all contributions to it.

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

Defintion

Using the type of subsets in a universe

Using sigma-frames

Type of Dedekind cut structures

See also

References