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

Β Defintion

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:

isInhabited 𝒰(P)≔[𝒯 𝒰(P)]isInhabited_\mathcal{U}(P) \coloneqq \left[\mathcal{T}_\mathcal{U}(P)\right]
isDownwardsClosed 𝒰(P)β‰”βˆ a:𝒯 𝒰(P)∏ b:T((b<a)β†’[fiber(ΞΉ P,b)])isDownwardsClosed_\mathcal{U}(P) \coloneqq \prod_{a:\mathcal{T}_\mathcal{U}(P)} \prod_{b:T} \left((b \lt a) \to \left[fiber(\iota_P,b)\right]\right)
isUpwardsClosed 𝒰(P)β‰”βˆ a:𝒯 𝒰(P)∏ b:T((a<b)β†’[fiber(ΞΉ P,b)])isUpwardsClosed_\mathcal{U}(P) \coloneqq \prod_{a:\mathcal{T}_\mathcal{U}(P)} \prod_{b:T} \left((a \lt b) \to \left[\fiber(\iota_P,b)\right]\right)
isDownwardsOpen 𝒰(P)β‰”βˆ a:𝒯 𝒰(P)[βˆ‘ b:𝒯 𝒰(P)a<b]isDownwardsOpen_\mathcal{U}(P) \coloneqq \prod_{a:\mathcal{T}_\mathcal{U}(P)} \left[\sum_{b:\mathcal{T}_\mathcal{U}(P)} a \lt b\right]
isUpwardsOpen 𝒰(P)β‰”βˆ a:𝒯 𝒰(P)[βˆ‘ b:𝒯 𝒰(P)b<a]isUpwardsOpen_\mathcal{U}(P) \coloneqq \prod_{a:\mathcal{T}_\mathcal{U}(P)} \left[\sum_{b:\mathcal{T}_\mathcal{U}(P)} b \lt a\right]

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:

isLocated 𝒰(L,R)β‰”βˆ a:T∏ b:T((a<b)β†’[fiber(ΞΉ L,a)+fiber(ΞΉ R,b)])isLocated_\mathcal{U}(L, R) \coloneqq \prod_{a:T} \prod_{b:T} \left((a \lt b) \to \left[fiber(\iota_L,a) + fiber(\iota_R,b)\right]\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))
isBounded 𝒰(L,R)≔isInhabited 𝒰(L)Γ—isInhabited 𝒰(R)isBounded_\mathcal{U}(L, R) \coloneqq isInhabited_\mathcal{U}(L) \times isInhabited_\mathcal{U}(R)
isOpen 𝒰(L,R)≔isDownwardsOpen 𝒰(L)Γ—isUpwardsOpen 𝒰(R)isOpen_\mathcal{U}(L, R) \coloneqq isDownwardsOpen_\mathcal{U}(L) \times isUpwardsOpen_\mathcal{U}(R)
isRounded 𝒰(L,R)≔isDownwardsClosed 𝒰(L)Γ—isUpwardsClosed 𝒰(R)isRounded_\mathcal{U}(L, R) \coloneqq isDownwardsClosed_\mathcal{U}(L) \times isUpwardsClosed_\mathcal{U}(R)
isDedekindCut 𝒰(L,R)≔isBounded 𝒰(L,R)Γ—isOpen 𝒰(L,R)Γ—isRounded 𝒰(L,R)Γ—isLocated 𝒰(L,R)Γ—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)

(L,R)(L, R) is a 𝒰\mathcal{U}-Dedekind cut if it comes with a term Ξ΄:isDedekindCut 𝒰(L,R)\delta:isDedekindCut_\mathcal{U}(L, R).

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

DedekindCut 𝒰(T)β‰”βˆ‘ (L,R):Sub 𝒰(T)Γ—Sub 𝒰(T)isDedekindCut 𝒰(L,R)DedekindCut_\mathcal{U}(T) \coloneqq \sum_{(L, R):Sub_\mathcal{U}(T) \times Sub_\mathcal{U}(T)} isDedekindCut_\mathcal{U}(L, R)

Using open intervals

Given a type TT with a dense strict order <\lt, let us define the family of lower bounded open intervals a:T⊒(a,∞)a:T \vdash (a,\infty) and upper bounded open intervals a:T⊒(βˆ’βˆž,a)a:T \vdash (-\infty, a). The type of 𝒰\mathcal{U}-Dedekind cuts in a universe 𝒰\mathcal{U} is a frame generated by (a,∞)(a,\infty) and (βˆ’βˆž,a)(-\infty, a) such that

TβŠ†β‹ƒ a:T 𝒰(a,∞)T \subseteq \bigcup_{a:T}^\mathcal{U} (a,\infty)
TβŠ†β‹ƒ a:T 𝒰(βˆ’βˆž,a)T \subseteq \bigcup_{a:T}^\mathcal{U} (-\infty,a)
∏ a:T∏ b:T(a<b)β†’((b,∞)βŠ†(a,∞))\prod_{a:T} \prod_{b:T} (a \lt b) \to ((b,\infty) \subseteq (a,\infty))
∏ a:T∏ b:T(b<a)β†’((βˆ’βˆž,b)βŠ†(βˆ’βˆž,a))\prod_{a:T} \prod_{b:T} (b \lt a) \to ((-\infty,b) \subseteq (-\infty,a))
∏ a:T(a,∞)βŠ†β‹ƒ b:(a,∞) 𝒰(b,∞)\prod_{a:T} (a,\infty) \subseteq \bigcup_{b:(a,\infty)}^\mathcal{U} (b,\infty)
∏ a:T(βˆ’βˆž,a)βŠ†β‹ƒ b:(βˆ’βˆž,a) 𝒰(βˆ’βˆž,b)\prod_{a:T} (-\infty,a) \subseteq \bigcup_{b:(-\infty,a)}^\mathcal{U} (-\infty,b)
∏ a:T∏ b:T(a<b)β†’TβŠ†(a,∞)βˆͺ(βˆ’βˆž,b)\prod_{a:T} \prod_{b:T} (a \lt b) \to T \subseteq (a, \infty) \cup (-\infty, b)
∏ a:T∏ b:T(a,∞)∩(βˆ’βˆž,b)βŠ†(a,b)\prod_{a:T} \prod_{b:T} (a,\infty) \cap (-\infty,b) \subseteq (a,b)

A 𝒰\mathcal{U}-Dedekind cut is an element of this frame.

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

isInhabited Ξ£(P)≔[fiber(P,⊀)]isInhabited_\Sigma(P) \coloneqq \left[fiber(P,\top)\right]
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:fiber(P,⊀)∏ b:T(a<b)β†’(P(b)=⊀)isUpwardsClosed_\Sigma(P) \coloneqq \prod_{a:fiber(P,\top)} \prod_{b:T} (a \lt b) \to (P(b) = \top)
isDownwardsOpen Ξ£(P)β‰”βˆ a:fiber(P,⊀)β†’[βˆ‘ b:fiber(P,⊀)(a<b)]isDownwardsOpen_\Sigma(P) \coloneqq \prod_{a:fiber(P,\top)} \to \left[\sum_{b:fiber(P,\top)} (a \lt b)\right]
isUpwardsOpen Ξ£(P)β‰”βˆ a:fiber(P,⊀)β†’[βˆ‘ b:fiber(P,⊀)(b<a)]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β†’Ξ£)Γ—(Tβ†’Ξ£)(L, R):(T \to \Sigma) \times (T \to \Sigma) in a universe 𝒰\mathcal{U}, let us define the following propositions:

isLocated Ξ£(L,R)β‰”βˆ a:T∏ b:T((a<b)β†’[(L(a)=⊀)+(R(b)=⊀)])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 Ξ£(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)
isBounded Ξ£(L,R)≔isInhabited Ξ£(L)Γ—isInhabited Ξ£(R)isBounded_\Sigma(L, R) \coloneqq isInhabited_\Sigma(L) \times isInhabited_\Sigma(R)
isOpen Ξ£(L,R)≔isDownwardsOpen Ξ£(L)Γ—isUpwardsOpen Ξ£(R)isOpen_\Sigma(L, R) \coloneqq isDownwardsOpen_\Sigma(L) \times isUpwardsOpen_\Sigma(R)
isRounded Ξ£(L,R)≔isDownwardsClosed Ξ£(L)Γ—isUpwardsClosed Ξ£(R)isRounded_\Sigma(L, R) \coloneqq isDownwardsClosed_\Sigma(L) \times isUpwardsClosed_\Sigma(R)
isDedekindCut Ξ£(L,R)≔isBounded Ξ£(L,R)Γ—isOpen Ξ£(L,R)Γ—isRounded Ξ£(L,R)Γ—isLocated Ξ£(L,R)Γ—isTransitive Ξ£(L,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)(L, R) is a Ξ£\Sigma-Dedekind cut if it comes with a term Ξ΄:isDedekindCut Ξ£(L,R)\delta:isDedekindCut_\Sigma(L, R).

The type of Ξ£\Sigma-Dedekind cuts of TT for a Οƒ\sigma-frame Ξ£\Sigma is defined as

DedekindCut Ξ£(T)β‰”βˆ‘ (L,R):(Tβ†’Ξ£)Γ—(Tβ†’Ξ£)isDedekindCut Ξ£(L,R)DedekindCut_\Sigma(T) \coloneqq \sum_{(L, R):(T \to \Sigma) \times (T \to \Sigma)} isDedekindCut_\Sigma(L, R)

Β See also


Revision on April 22, 2022 at 01:37:51 by Anonymous?. See the history of this page for a list of all contributions to it.