Homotopy Type Theory
Dedekind cut > history (Rev #3, changes)
Showing changes from revision #2 to #3:
Added | Removed | Changed
Β 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:
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 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)) 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 π° \mathcal{U} -Dedekind cut if it comes with a term Ξ΄ : isDedekindCut π° ( L , R ) \delta:isDedekindCut_\mathcal{U}(L, R) .
The type of π° \mathcal{U} -Dedekind cuts of T T 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)
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:
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 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) 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) isDedekindCut Ξ£ ( L , R ) β isBounded Ξ£ ( L , R ) Γ isOpen Ξ£ ( L , R ) Γ isRounded Ξ£ ( L , R ) Γ isLocated Ξ£ ( L , R ) Γ isTransitive Ξ£ ( L , R ) isDedekindCut_\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 -Dedekind cut if it comes with a term Ξ΄ : isDedekindCut Ξ£ ( L , R ) \delta:isDedekindCut_\Sigma(L, R) .
The type of Ξ£ \Sigma -Dedekind cuts of T T for a Ο \sigma -frame Ξ£ \Sigma is defined as
DedekindCut Ξ£ ( T ) β β ( L , R ) : ( T β Ξ£ ) Γ ( T β Ξ£ ) isDedekindCut Ξ£ ( L , R ) DedekindCut_\Sigma(T) \coloneqq \sum_{(L, R):(T \to \Sigma) \times (T \to \Sigma)} isDedekindCut_\Sigma(L, R)
Β See also
References
Revision on April 21, 2022 at 22:51:39 by
Anonymous? .
See the history of this page for a list of all contributions to it.