Homotopy Type Theory
extended Dedekind cut > history (Rev #1)
Defintion
Using the type of subsets in a universe
Given a type T T with a dense strict order < \lt , and given a subtype P : Sub 𝒰 ( T ) P:Sub_\mathcal{U}(T) with monic function i P : 𝒯 𝒰 ( P ) → T i_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 function s i L : 𝒯 𝒰 ( L ) → T i_L:\mathcal{T}_\mathcal{U}(L) \to T and i R : 𝒯 𝒰 ( R ) → T i_R:\mathcal{T}_\mathcal{U}(R) \to T , let us define the following proposition s:
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 extended 𝒰 \mathcal{U} -Dedekind cut if it comes with a term δ : isExtendedDedekindCut 𝒰 ( L , R ) \delta:isExtendedDedekindCut_\mathcal{U}(L, R) .
The type of extended 𝒰 \mathcal{U} -Dedekind cuts of T T 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)
Using sigma-frames
Given a type T T 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 proposition s:
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 T T 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 11:18:27 by
Anonymous? .
See the history of this page for a list of all contributions to it.