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

Showing changes from revision #2 to #3: Added | Removed | Changed

Defintion

< Dedekind cut

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:

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))
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)
isExtendedDedekindCut 𝒰(L,R)isOpen 𝒰(L,R)×isRounded 𝒰(L,R)×isLocated 𝒰(L,R)×isTransitive 𝒰(L,R)isExtendedDedekindCut_\mathcal{U}(L, R) \coloneqq 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 locally 𝒰\mathcal{U}-small extended Dedekind cut if it comes with a term δ:isExtendedDedekindCut 𝒰(L,R)\delta:isExtendedDedekindCut_\mathcal{U}(L, R).

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

ExtendedDedekindCut 𝒰(T) (L,R):Sub 𝒰(T)×Sub 𝒰(T)isExtendedDedekindCut 𝒰(L,R)ExtendedDedekindCut_\mathcal{U}(T) \coloneqq \sum_{(L, R):Sub_\mathcal{U}(T) \times Sub_\mathcal{U}(T)} isExtendedDedekindCut_\mathcal{U}(L, R)

See also

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