Principle of Global Choice
Table of Contents
1 The Principle of Global Choice
module Lib.GlobalChoice where
The principle of global choice states that, from an inhabitant of the propositional truncation of a type, one can get an inhabitant of the type. This file defines this notion, and exhibits some conditions for a type to satisfy the principle of global choice.
1.1 Packages imports
The imported packages can be accessed via the following links:
import Lib.PropTrunc import Lib.Prop.Fin import Lib.Prop.Nat
1.2 Principle of Global Choice
global-choice (A : U) : U = Prop-trunc A → A
1.3 Decidable subtype of natural numbers implies global choice
In this section, we show that if P is a subtype of Nat such that each P(n) is decidable, then Σn: NatP(n) satisfies the principle of global choice. For this, we use the well-ordering principle. The first thing we need to do is to show that Σ(n: Nat)P(n) × is-lower-boundP(n) is a proposition.
well-ordering/is-prop (P : Nat → U) (H : (n : Nat) → is-prop (P n)) : is-prop (Σ Nat (λn. (P n) * (is-lower-bound P n))) = λt u. SgPath-prop Nat ( λn. (P n) * (is-lower-bound P n)) ( λn. is-prop/prod ( P n) ( is-lower-bound P n) ( H n) ( is-prop/pi Nat ( λx. P x → Prop/type (le n x)) ( λx. is-prop/pi ( P x) ( λ_. Prop/type (le n x)) ( λ_. Prop/is-prop (le n x))))) t u ( le/is-antisymmetric t.1 u.1 ( t.2.2 u.1 u.2.1) ( u.2.2 t.1 t.2.1)) well-ordering/Prop (P : Nat → UU-Prop) : UU-Prop = ( Σ Nat (λn. (Prop/type (P n)) * (is-lower-bound (λx. Prop/type (P x)) n)), well-ordering/is-prop ( λx. Prop/type (P x)) ( λx. Prop/is-prop (P x)))
By the recursion principle of propositional truncation, there is a map between || Σ(x: Nat)P(x) || to Σ(x: Nat)P(x) × is-lower-boundP(x).
well-ordering/map (P : Nat → UU-Prop) (H : (x : Nat) → is-decidable (Prop/type (P x))) : Prop-trunc (Σ Nat (λx. Prop/type (P x))) → Σ Nat (λn. (Prop/type (P n)) * (is-lower-bound (λx. Prop/type (P x)) n)) = rec-Prop-trunc ( Σ Nat (λx. Prop/type (P x))) ( well-ordering/Prop P) ( well-ordering-principle ( λx. Prop/type (P x)) H)
Hence, there's a map out of the propositional truncation of Σ(x: Nat)P(x).
Nat-decidable-subtype/global-choice (P : Nat → UU-Prop) (H : (x : Nat) → is-decidable (Prop/type (P x))) : global-choice (Σ Nat (λx. Prop/type (P x))) = λp. let t : Σ Nat (λn. (Prop/type (P n)) * (is-lower-bound (λx. Prop/type (P x)) n)) = well-ordering/map P H p in ( t.1, t.2.1)
As a corollary, any decidable subtype over Fin k also satisfies the global choice. Indeed, we have the equivalence Σ(x: Fin k)P(x) ≅ Σ(n: Nat)Σ(p: n<k)P(e(n, p)). We must show that it is still a decidable proposition. It is not a problem, as both < and P are decidable propositions.
Fin-Nat-family/is-prop (k : Nat) (P : Fin k → UU-Prop) (n : Nat) : is-prop (Fin-Nat-family k (λx. Prop/type (P x)) n) = λt u. SgPath-prop ( Prop/type (lt n k)) ( λp. Prop/type (P (Fin/from-classical-Fin k (n, p)))) ( λp. Prop/is-prop (P (Fin/from-classical-Fin k (n, p)))) t u ( Prop/is-prop (lt n k) t.1 u.1) Fin-Nat-family/Prop (k : Nat) (P : Fin k → UU-Prop) (n : Nat) : UU-Prop = ( Fin-Nat-family k (λx. Prop/type (P x)) n, Fin-Nat-family/is-prop k P n) Fin-Nat-family/is-decidable'' (k : Nat) (P : Fin k → UU-Prop) (n : Nat) (p : Prop/type (lt n k)) : Coprod (Prop/type (P (Fin/from-classical-Fin k (n, p)))) (neg (Prop/type (P (Fin/from-classical-Fin k (n, p))))) → is-decidable (Fin-Nat-family k (λx. Prop/type (P x)) n) = split inl x → inl (p, x) inr np → inr (λt. np ( tr ( Prop/type (lt n k)) t.1 p ( Prop/is-prop (lt n k) t.1 p) ( λq. Prop/type (P (Fin/from-classical-Fin k (n, q)))) t.2)) Fin-Nat-family/is-decidable' (k : Nat) (P : Fin k → UU-Prop) (d : (x : Fin k) → is-decidable (Prop/type (P x))) (n : Nat) : Coprod (Prop/type (lt n k)) (neg (Prop/type (lt n k))) → is-decidable (Fin-Nat-family k (λx. Prop/type (P x)) n) = split inl p → Fin-Nat-family/is-decidable'' k P n p (d (Fin/from-classical-Fin k (n, p))) inr nlt → inr (λt. nlt t.1) Fin-Nat-family/is-decidable (k : Nat) (P : Fin k → UU-Prop) (d : (x : Fin k) → is-decidable (Prop/type (P x))) (n : Nat) : is-decidable (Fin-Nat-family k (λx. Prop/type (P x)) n) = Fin-Nat-family/is-decidable' k P d n ( lt/is-decidable n k)
As such, we can show the result.
decidable-subtype/global-choice' (k : Nat) (P : Fin k → UU-Prop) (d : (x : Fin k) → is-decidable (Prop/type (P x))) : global-choice (Σ (Fin k) (λx. Prop/type (P x))) = λp. Equiv/inv-map ( Σ (Fin k) (λx. Prop/type (P x))) ( Σ Nat (Fin-Nat-family k (λx. Prop/type (P x)))) ( Fin-Nat-family/Equiv k (λx. Prop/type (P x))) ( Nat-decidable-subtype/global-choice ( Fin-Nat-family/Prop k P) ( Fin-Nat-family/is-decidable k P d) ( Prop-trunc/map ( Σ (Fin k) (λx. Prop/type (P x))) ( Σ Nat (Fin-Nat-family k (λx. Prop/type (P x)))) ( Equiv/map ( Σ (Fin k) (λx. Prop/type (P x))) ( Σ Nat (Fin-Nat-family k (λx. Prop/type (P x)))) ( Fin-Nat-family/Equiv k (λx. Prop/type (P x)))) p))
A more useful statement for this lemma is as follows:
lock decidable-subtype/global-choice' decidable-subtype/global-choice (A : U) (k : Nat) (e : Equiv (Fin k) A) (P : A → UU-Prop) (d : (x : A) → is-decidable (Prop/type (P x))) : global-choice (Σ A (λx. Prop/type (P x))) = λp. let B : Fin k → UU-Prop = λx. P (Equiv/map (Fin k) A e x) f : Fin k → A = Equiv/map (Fin k) A e g : A → Fin k = Equiv/inv-map (Fin k) A e u : Σ (Fin k) (λx. Prop/type (B x)) = decidable-subtype/global-choice' k B ( λx. d (f x)) ( rec-Prop-trunc ( Σ A (λx. Prop/type (P x))) ( Prop-trunc/Prop (Σ (Fin k) (λx. Prop/type (B x)))) ( λt. Prop-trunc/unit ( g t.1, tr A t.1 (f (g t.1)) ( inv A (f (g t.1)) t.1 (Equiv/inv-right-htpy (Fin k) A e t.1)) ( λx. Prop/type (P x)) t.2)) p) in ( f u.1, u.2) unlock decidable-subtype/global-choice'
Another result would be:
count/global-choice (A : U) : (k : Nat) (e : Equiv (Fin k) A) → global-choice A = split zero → λe a. ex-falso A ( rec-Prop-trunc A ( Empty/Prop) ( λx. Equiv/inv-map Empty A e x) a) suc k → λe _. Equiv/map (Fin (suc k)) A e (zero-Fin k)