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

Defintion

Wherever you see an order proposition, replace with a open interval. Whenever you see an existential quantifier with an order proposition, replace with a lower/upper unbounded open interval. This should result in actual structure as (dependent) functions between sets for all 8 properties.

Using the type of subsets in a universe

Given a type TT with a dense strict order <\lt, and given a subtype P:Sub 𝒰(T)P:Sub_\mathcal{U}(T) with monic function i P:𝒯 𝒰(P)Ti_P:\mathcal{T}_\mathcal{U}(P) \to T, let us define the following propositions:

Inhabitor 𝒰(P)𝒯 𝒰(P)Inhabitor_\mathcal{U}(P) \coloneqq \mathcal{T}_\mathcal{U}(P)
DownwardsCloser 𝒰(P) a:𝒯 𝒰(P) b:T((b<a)fiber(ι P,b))DownwardsCloser_\mathcal{U}(P) \coloneqq \prod_{a:\mathcal{T}_\mathcal{U}(P)} \prod_{b:T} \left((b \lt a) \to fiber(\iota_P,b)\right)
UpwardsCloser 𝒰(P) a:𝒯 𝒰(P) b:T((a<b)fiber(ι P,b))UpwardsCloser_\mathcal{U}(P) \coloneqq \prod_{a:\mathcal{T}_\mathcal{U}(P)} \prod_{b:T} \left((a \lt b) \to fiber(\iota_P,b)\right)
DownwardsOpener 𝒰(P) a:𝒯 𝒰(P) b:𝒯 𝒰(P)a<bDownwardsOpener_\mathcal{U}(P) \coloneqq \prod_{a:\mathcal{T}_\mathcal{U}(P)} \sum_{b:\mathcal{T}_\mathcal{U}(P)} a \lt b
UpwardsOpener 𝒰(P) a:𝒯 𝒰(P) b:𝒯 𝒰(P)b<aUpwardsOpener_\mathcal{U}(P) \coloneqq \prod_{a:\mathcal{T}_\mathcal{U}(P)} \sum_{b:\mathcal{T}_\mathcal{U}(P)} b \lt a

Given a pair of subtypes (L,R):Sub 𝒰(T)×Sub 𝒰(T)(L, R):Sub_\mathcal{U}(T) \times Sub_\mathcal{U}(T) in a universe 𝒰\mathcal{U} with monic functions i L:𝒯 𝒰(L)Ti_L:\mathcal{T}_\mathcal{U}(L) \to T and i R:𝒯 𝒰(R)Ti_R:\mathcal{T}_\mathcal{U}(R) \to T, let us define the following propositions:

Locator 𝒰(L,R) a:T b:T((a<b)(fiber(ι L,A)+fiber(ι R,b)))Locator_\mathcal{U}(L, R) \coloneqq \prod_{a:T} \prod_{b:T} \left((a \lt b) \to (fiber(\iota_L,A) + fiber(\iota_R,b))\right)
isTransitive 𝒰(L,R) a:𝒯 𝒰(L) b:𝒯 𝒰(R)(i L(a)<i L(b))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 𝒰(L,R)Inhabitor 𝒰(L)×Inhabitor 𝒰(R)Bounder_\mathcal{U}(L, R) \coloneqq Inhabitor_\mathcal{U}(L) \times Inhabitor_\mathcal{U}(R)
Rounder 𝒰(L,R)DownwardsCloser 𝒰(L)×UpwardsCloser 𝒰(R)Rounder_\mathcal{U}(L, R) \coloneqq DownwardsCloser_\mathcal{U}(L) \times UpwardsCloser_\mathcal{U}(R)
Opener 𝒰(L,R)DownwardsOpener 𝒰(L)×UpwardsOpener 𝒰(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)(L, R) is defined as

DedekindCutStructure 𝒰(L,R)Bounder 𝒰(L,R)×Rounder 𝒰(L,R)×Opener 𝒰(L,R)×Locator 𝒰(L,R)×isTransitive 𝒰(L,R)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)(L, R) is simply a term Δ:DedekindCutStructure 𝒰(L,R)\Delta:DedekindCutStructure_\mathcal{U}(L, R).

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

Using sigma-frames

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

Inhabitor Σ(P)fiber(P,)Inhabitor_\Sigma(P) \coloneqq fiber(P,\top)
isDownwardsClosed Σ(P) a:fiber(P,) b:T(b<a)(P(b)=)isDownwardsClosed_\Sigma(P) \coloneqq \prod_{a:fiber(P,\top)} \prod_{b:T} (b \lt a) \to (P(b) = \top)
isUpwardsClosed Σ(P) a:Tfiber(P,) b:T(a<b)(P(b)=)isUpwardsClosed_\Sigma(P) \coloneqq \prod_{a:Tfiber(P,\top)} \prod_{b:T} (a \lt b) \to (P(b) = \top)
DownwardsOpener Σ(P) a:fiber(P,) b:fiber(P,)(a<b)DownwardsOpener_\Sigma(P) \coloneqq \prod_{a:fiber(P,\top)} \sum_{b:fiber(P,\top)} (a \lt b)
UpwardsOpener Σ(P) a:fiber(P,) b:fiber(P,)(b<a)UpwardsOpener_\Sigma(P) \coloneqq \prod_{a:fiber(P,\top)} \sum_{b:fiber(P,\top)} (b \lt a)

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

Locator Σ(L,R) a:T b:T((a<b)((L(a)=)+(R(b)=)))Locator_\Sigma(L, R) \coloneqq \prod_{a:T} \prod_{b:T} \left((a \lt b) \to ((L(a) = \top) + (R(b) = \top))\right)
isTransitive Σ(L,R) a:fiber(L,) b:fiber(R,)(a<b)isTransitive_\Sigma(L, R) \coloneqq \prod_{a:fiber(L,\top)} \prod_{b:fiber(R,\top)} (a \lt b)
Bounder Σ(L,R)Inhabitor Σ(L)×Inhabitor Σ(R)Bounder_\Sigma(L, R) \coloneqq Inhabitor_\Sigma(L) \times Inhabitor_\Sigma(R)
isRounded Σ(L,R)isDownwardsClosed Σ(L)×isUpwardsClosed Σ(R)isRounded_\Sigma(L, R) \coloneqq isDownwardsClosed_\Sigma(L) \times isUpwardsClosed_\Sigma(R)
Opener Σ(L,R)DownwardsOpener Σ(L)×UpwardsOpener Σ(R)Opener_\Sigma(L, R) \coloneqq DownwardsOpener_\Sigma(L) \times UpwardsOpener_\Sigma(R)

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

isDedekindCut Σ(L,R)Bounder Σ(L,R)×Opener Σ(L,R)×isRounded Σ(L,R)×Locator Σ(L,R)×isTransitive Σ(L,R)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)(L, R) is simply a term Δ:DedekindCutStructure Σ(L,R)\Delta:DedekindCutStructure_\Sigma(L, R).

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

See also

References

Revision on June 10, 2022 at 03:09:25 by Anonymous?. See the history of this page for a list of all contributions to it.