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

Β Defintion

Given a type TT with a dense strict order <\lt, and 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:

isInhabited 𝒰(L)≔[𝒯 𝒰(L)]isInhabited_\mathcal{U}(L) \coloneqq \left[\mathcal{T}_\mathcal{U}(L)\right]
isInhabited 𝒰(R)≔β R:[𝒯 𝒰(R)]isInhabited_\mathcal{U}(R) \coloneqq \beta_R:\left[\mathcal{T}_\mathcal{U}(R)\right]
isDownwardsClosed 𝒰(L)β‰”βˆ a:𝒯 𝒰(L)∏ b:T((b<a)β†’[βˆ‘ c:𝒯 𝒰(L)ΞΉ L(c)=b])isDownwardsClosed_\mathcal{U}(L) \coloneqq \prod_{a:\mathcal{T}_\mathcal{U}(L)} \prod_{b:T} \left((b \lt a) \to \left[\sum_{c:\mathcal{T}_\mathcal{U}(L)} \iota_L(c) = b\right]\right)
isUpwardsClosed 𝒰(R)β‰”βˆ a:𝒯 𝒰(R)∏ b:T((a<b)β†’[βˆ‘ c:𝒯 𝒰(R)ΞΉ R(c)=b])isUpwardsClosed_\mathcal{U}(R) \coloneqq \prod_{a:\mathcal{T}_\mathcal{U}(R)} \prod_{b:T} \left((a \lt b) \to \left[\sum_{c:\mathcal{T}_\mathcal{U}(R)} \iota_R(c) = b\right]\right)
isDownwardsOpen 𝒰(L)β‰”βˆ a:𝒯 𝒰(L)[βˆ‘ b:𝒯 𝒰(L)a<b]isDownwardsOpen_\mathcal{U}(L) \coloneqq \prod_{a:\mathcal{T}_\mathcal{U}(L)} \left[\sum_{b:\mathcal{T}_\mathcal{U}(L)} a \lt b\right]
isUpwardsOpen 𝒰(R)β‰”βˆ a:𝒯 𝒰(R)[βˆ‘ b:𝒯 𝒰(R)b<a]isUpwardsOpen_\mathcal{U}(R) \coloneqq \prod_{a:\mathcal{T}_\mathcal{U}(R)} \left[\sum_{b:\mathcal{T}_\mathcal{U}(R)} b \lt a\right]
isLocated 𝒰(L,R)β‰”βˆ a:T∏ b:T((a<b)β†’[[βˆ‘ c:𝒯 𝒰(L)ΞΉ L(c)=a]+[βˆ‘ c:𝒯 𝒰(R)ΞΉ R(c)=b]])isLocated_\mathcal{U}(L, R) \coloneqq \prod_{a:T} \prod_{b:T} \left((a \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 𝒰(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 Dedekind cut if it comes with a term Ξ΄:isDedekindCut 𝒰(L,R)\delta:isDedekindCut_\mathcal{U}(L, R).

Β Type of Dedekind cuts

The type of 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)

Β See also

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