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

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


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:

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)
isIntervalCut 𝒰(L,R)isBounded 𝒰(L,R)×isOpen 𝒰(L,R)×isRounded 𝒰(L,R)×isTransitive 𝒰(L,R)isIntervalCut_\mathcal{U}(L, R) \coloneqq isBounded_\mathcal{U}(L, R) \times isOpen_\mathcal{U}(L, R) \times isRounded_\mathcal{U}(L, R) \times isTransitive_\mathcal{U}(L, R)

(L,R)(L, R) is a 𝒰\mathcal{U}-interval cut if it comes with a term δ:isIntervalCut 𝒰(L,R)\delta:isIntervalCut_\mathcal{U}(L, R).

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

IntervalCut 𝒰(T) (L,R):Sub 𝒰(T)×Sub 𝒰(T)isIntervalCut 𝒰(L,R)IntervalCut_\mathcal{U}(T) \coloneqq \sum_{(L, R):Sub_\mathcal{U}(T) \times Sub_\mathcal{U}(T)} isIntervalCut_\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}-interval 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)(a,b)\prod_{a:T} \prod_{b:T} (a,\infty) \cap (-\infty,b) \subseteq (a,b)

A 𝒰\mathcal{U}-interval 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:

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)
isIntervalCut Σ(L,R)isBounded Σ(L,R)×isOpen Σ(L,R)×isRounded Σ(L,R)×isLocated Σ(L,R)×isTransitive Σ(L,R)isIntervalCut_\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-interval cut if it comes with a term δ:isIntervalCut Σ(L,R)\delta:isIntervalCut_\Sigma(L, R).

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

IntervalCut Σ(T) (L,R):(TΣ)×(TΣ)isIntervalCut Σ(L,R)IntervalCut_\Sigma(T) \coloneqq \sum_{(L, R):(T \to \Sigma) \times (T \to \Sigma)} isIntervalCut_\Sigma(L, R)

See also

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