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

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

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:

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)
isDownwardsClosed isDownwardsOpen 𝒰(P) a:𝒯 𝒰(P) b:T[ b:𝒯 𝒰(P)a<b]((b<a)[fiber(ι P,b)]) isDownwardsClosed_\mathcal{U}(P) isDownwardsOpen_\mathcal{U}(P) \coloneqq \prod_{a:\mathcal{T}_\mathcal{U}(P)} \prod_{b:T} \left[\sum_{b:\mathcal{T}_\mathcal{U}(P)} \left((b a \lt a) b\right] \to \left[fiber(\iota_P,b)\right]\right)
isUpwardsClosed isUpwardsOpen 𝒰(P) a:𝒯 𝒰(P) b:T[ b:𝒯 𝒰(P)b<a]((a<b)[fiber(ι P,b)]) isUpwardsClosed_\mathcal{U}(P) isUpwardsOpen_\mathcal{U}(P) \coloneqq \prod_{a:\mathcal{T}_\mathcal{U}(P)} \prod_{b:T} \left[\sum_{b:\mathcal{T}_\mathcal{U}(P)} \left((a b \lt b) a\right] \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:

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))
isLocated isOpen 𝒰(L,R) a:TisDownwardsOpen 𝒰 b:T(((a<b)[fiber(ι L,a)+fiber(ι R,b)])L)×isUpwardsOpen 𝒰(R) isLocated_\mathcal{U}(L, isOpen_\mathcal{U}(L, R) \coloneqq \prod_{a:T} isDownwardsOpen_\mathcal{U}(L) \prod_{b:T} \times \left((a isUpwardsOpen_\mathcal{U}(R) \lt b) \to \left[fiber(\iota_L,a) + fiber(\iota_R,b)\right]\right)
isTransitive isRounded 𝒰(L,R) a:𝒯 𝒰(L)isDownwardsClosed 𝒰 b:𝒯 𝒰(R)(i LL(a) < × i isUpwardsClosed L 𝒰( b R)) isTransitive_\mathcal{U}(L, isRounded_\mathcal{U}(L, R) \coloneqq \prod_{a:\mathcal{T}_\mathcal{U}(L)} isDownwardsClosed_\mathcal{U}(L) \prod_{b:\mathcal{T}_\mathcal{U}(R)} \times (i_L(a) isUpwardsClosed_\mathcal{U}(R) \lt i_L(b))
isOpen isExtendedDedekindCut 𝒰(L,R) isDownwardsOpen isOpen 𝒰(L,R)× isUpwardsOpen isRounded 𝒰(L,R)×isLocated 𝒰(L,R)×isTransitive 𝒰(L,R) isOpen_\mathcal{U}(L, isExtendedDedekindCut_\mathcal{U}(L, R) \coloneqq isDownwardsOpen_\mathcal{U}(L) isOpen_\mathcal{U}(L, R) \times isUpwardsOpen_\mathcal{U}(R) isRounded_\mathcal{U}(L, R) \times isLocated_\mathcal{U}(L, R) \times isTransitive_\mathcal{U}(L, 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).

(L,R)(L, R)The type of locally is a 𝒰\mathcal{U}extended 𝒰\mathcal{U}-Dedekind cut-small extended Dedekind cuts of if it comes with a term TTδ:isExtendedDedekindCut 𝒰(L,R)\delta:isExtendedDedekindCut_\mathcal{U}(L, R) in a universe .𝒰\mathcal{U} is defined as

The type of extended 𝒰\mathcal{U}-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)
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)

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:

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)
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)
isExtendedDedekindCut Σ(L,R)isOpen Σ(L,R)×isRounded Σ(L,R)×isLocated Σ(L,R)×isTransitive Σ(L,R)isExtendedDedekindCut_\Sigma(L, R) \coloneqq isOpen_\Sigma(L, R) \times isRounded_\Sigma(L, R) \times isLocated_\Sigma(L, R) \times isTransitive_\Sigma(L, R)

(L,R)(L, R) is an extended Σ\Sigma-Dedekind cut if it comes with a term δ:isExtendedDedekindCut Σ(L,R)\delta:isExtendedDedekindCut_\Sigma(L, R).

The type of extended Σ\Sigma-Dedekind cuts of TT for a σ\sigma-frame Σ\Sigma is defined as

ExtendedDedekindCut Σ(T) (L,R):(TΣ)×(TΣ)isExtendedDedekindCut Σ(L,R)ExtendedDedekindCut_\Sigma(T) \coloneqq \sum_{(L, R):(T \to \Sigma) \times (T \to \Sigma)} isExtendedDedekindCut_\Sigma(L, R)

See also

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