Homotopy Type Theory Dedekind cut > 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$ , 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:

Using the type of subsets in a universe

~~$isInhabited_\mathcal{U}(L) \coloneqq \left[\mathcal{T}_\mathcal{U}(L)\right]$~~

Given a type $T$ with a dense strict order $\lt$ , and given a subtype $P:Sub_\mathcal{U}(T)$ with monic function $i_P:\mathcal{T}_\mathcal{U}(P) \to T$ , let us define the following propositions:

~~$isInhabited_\mathcal{U}(R) \coloneqq \beta_R:\left[\mathcal{T}_\mathcal{U}(R)\right]$~~

{isDownwardsClosed isInhabited}_{𝒰} (L P) ≔ \prod_{a : 𝒯_{𝒰} (L)} [𝒯_{𝒰} (P)] \prod_{b : T} ((b < a) \to [\sum_{c : 𝒯_{𝒰} (L)} ι_{L} (c) = b])

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

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

~~isUpwardsClosed_\mathcal{U}(R)~~ isDownwardsClosed_\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 ~~\left[\sum_{c:\mathcal{T}_\mathcal{U}(R)}~~ \left[fiber(\iota_P,b)\right]\right) ~~\iota_R(c)~~ = ~~b\right]\right)~~

{isDownwardsOpen isUpwardsClosed}_{𝒰} (L P) ≔ \prod_{a : 𝒯_{𝒰} (L P)} [\sum_{b : 𝒯_{𝒰} (L)} a < b] \prod_{b : T} ((a < b) \to [fiber (ι_{P}, b)])

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

{isUpwardsOpen isDownwardsOpen}_{𝒰} (R P) ≔ \prod_{a : 𝒯_{𝒰} (R P)} [\sum_{b : 𝒯_{𝒰} (R P)} b < a < b]

~~isUpwardsOpen_\mathcal{U}(R)~~ isDownwardsOpen_\mathcal{U}(P) \coloneqq ~~\prod_{a:\mathcal{T}_\mathcal{U}(R)}~~ \prod_{a:\mathcal{T}_\mathcal{U}(P)} ~~\left[\sum_{b:\mathcal{T}_\mathcal{U}(R)}~~ \left[\sum_{b:\mathcal{T}_\mathcal{U}(P)} b a \lt ~~a\right]~~ b\right]

{isLocated isUpwardsOpen}_{𝒰} (L P, R) ≔ \prod_{a : T 𝒯_{𝒰} (P)} \prod_{b : T} [\sum_{b : 𝒯_{𝒰} (P)} b < a] ((a < b) \to [[\sum_{c : 𝒯_{𝒰} (L)} ι_{L} (c) = a] + [\sum_{c : 𝒯_{𝒰} (R)} ι_{R} (c) = b]])

~~isLocated_\mathcal{U}(L,~~ isUpwardsOpen_\mathcal{U}(P) R) \coloneqq ~~\prod_{a:T}~~ \prod_{a:\mathcal{T}_\mathcal{U}(P)} ~~\prod_{b:T}~~ \left[\sum_{b:\mathcal{T}_\mathcal{U}(P)} ~~\left((a~~ b \lt b) ~~\to~~ ~~\left[\left[\sum_{c:\mathcal{T}_\mathcal{U}(L)}~~ ~~\iota_L(c)~~ = a\right] + ~~\left[\sum_{c:\mathcal{T}_\mathcal{U}(R)}~~ ~~\iota_R(c)~~ = ~~b\right]\right]\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))$~~
~~$isBounded_\mathcal{U}(L, R) \coloneqq isInhabited_\mathcal{U}(L) \times isInhabited_\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:

~~$isOpen_\mathcal{U}(L, R) \coloneqq isDownwardsOpen_\mathcal{U}(L) \times isUpwardsOpen_\mathcal{U}(R)$~~

{isRounded isLocated}_{𝒰} (L, R) ≔ {isDownwardsClosed}_{𝒰} \prod_{a : T} (\prod_{b : T} L ((a < b) \to [fiber (ι_{L}, a) + fiber (ι_{R}, b)])) \times {isUpwardsClosed}_{𝒰} (R)

~~isRounded_\mathcal{U}(L,~~ isLocated_\mathcal{U}(L, R) \coloneqq ~~isDownwardsClosed_\mathcal{U}(L)~~ \prod_{a:T} ~~\times~~ \prod_{b:T} ~~isUpwardsClosed_\mathcal{U}(R)~~ \left((a \lt b) \to \left[fiber(\iota_L,a) + fiber(\iota_R,b)\right]\right)

{isDedekindCut isTransitive}_{𝒰} (L, R) ≔ {isBounded}_{𝒰} \prod_{a : 𝒯_{𝒰} (L)} \prod_{b : 𝒯_{𝒰} (R)} (L i_{L}, R) \times {isOpen}_{𝒰} (L a, R) \times < {isRounded i}_{𝒰 L} (L b, R) \times {isLocated}_{𝒰} (L, R) \times {isTransitive}_{𝒰} (L, R)

~~isDedekindCut_\mathcal{U}(L,~~ R) ~~\coloneqq~~ ~~isBounded_\mathcal{U}(L,~~ R) ~~\times~~ ~~isOpen_\mathcal{U}(L,~~ R) ~~\times~~ ~~isRounded_\mathcal{U}(L,~~ R) ~~\times~~ ~~isLocated_\mathcal{U}(L,~~ R) ~~\times~~ 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))

isBounded_\mathcal{U}(L, R) \coloneqq isInhabited_\mathcal{U}(L) \times isInhabited_\mathcal{U}(R)

~~$(L, R)$ is a Dedekind cut if it comes with a term $\delta:isDedekindCut_\mathcal{U}(L, R)$ .~~

isOpen_\mathcal{U}(L, R) \coloneqq isDownwardsOpen_\mathcal{U}(L) \times isUpwardsOpen_\mathcal{U}(R)

isRounded_\mathcal{U}(L, R) \coloneqq isDownwardsClosed_\mathcal{U}(L) \times isUpwardsClosed_\mathcal{U}(R)

~~Type of Dedekind cuts~~

isDedekindCut_\mathcal{U}(L, R) \coloneqq isBounded_\mathcal{U}(L, R) \times isOpen_\mathcal{U}(L, R) \times isRounded_\mathcal{U}(L, R) \times isLocated_\mathcal{U}(L, R) \times isTransitive_\mathcal{U}(L, R)

~~The type of Dedekind cuts of~~ $(L, R)$ ~~$T$~~ is a ~~in a universe~~ $\mathcal{U}$ -Dedekind cut ~~$\mathcal{U}$~~ if it comes with a term ~~is defined as~~ $\delta:isDedekindCut_\mathcal{U}(L, R)$ .

~~$DedekindCut_\mathcal{U}(T) \coloneqq \sum_{(L, R):Sub_\mathcal{U}(T) \times Sub_\mathcal{U}(T)} isDedekindCut_\mathcal{U}(L, R)$~~

The type of $\mathcal{U}$ -Dedekind cuts of $T$ in a universe $\mathcal{U}$ is defined as

DedekindCut_\mathcal{U}(T) \coloneqq \sum_{(L, R):Sub_\mathcal{U}(T) \times Sub_\mathcal{U}(T)} isDedekindCut_\mathcal{U}(L, R)

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

isInhabited_\Sigma(P) \coloneqq \left[fiber(P,\top)\right]

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

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

isDownwardsOpen_\Sigma(P) \coloneqq \prod_{a:fiber(P,\top)} \to \left[\sum_{b:fiber(P,\top)} (a \lt b)\right]

isUpwardsOpen_\Sigma(P) \coloneqq \prod_{a:fiber(P,\top)} \to \left[\sum_{b:fiber(P,\top)} (b \lt a)\right]

Given a pair of open subtypes $(L, R):(T \to \Sigma) \times (T \to \Sigma)$ in a universe $\mathcal{U}$ , let us define the following propositions:

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

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

isBounded_\Sigma(L, R) \coloneqq isInhabited_\Sigma(L) \times isInhabited_\Sigma(R)

isOpen_\Sigma(L, R) \coloneqq isDownwardsOpen_\Sigma(L) \times isUpwardsOpen_\Sigma(R)

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

isDedekindCut_\Sigma(L, R) \coloneqq isBounded_\Sigma(L, R) \times isOpen_\Sigma(L, R) \times isRounded_\Sigma(L, R) \times isLocated_\Sigma(L, R) \times isTransitive_\Sigma(L, R)

$(L, R)$ is a $\Sigma$ -Dedekind cut if it comes with a term $\delta:isDedekindCut_\Sigma(L, R)$ .

The type of $\Sigma$ -Dedekind cuts of $T$ for a $\sigma$ -frame $\Sigma$ is defined as

DedekindCut_\Sigma(T) \coloneqq \sum_{(L, R):(T \to \Sigma) \times (T \to \Sigma)} isDedekindCut_\Sigma(L, R)

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:14:48 by Anonymous?. See the history of this page for a list of all contributions to it.

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

Defintion

Using the type of subsets in a universe

Type of Dedekind cuts

Using sigma-frames

See also

References