The axiom of choice
Content created by Egbert Rijke, Fredrik Bakke and Jonathan Prieto-Cubides.
Created on 2022-02-16.
Last modified on 2024-04-11.
module foundation.axiom-of-choice where
Imports
open import foundation.dependent-pair-types open import foundation.function-extensionality open import foundation.functoriality-propositional-truncation open import foundation.inhabited-types open import foundation.postcomposition-functions open import foundation.projective-types open import foundation.propositional-truncations open import foundation.sections open import foundation.split-surjective-maps open import foundation.surjective-maps open import foundation.universe-levels open import foundation-core.equivalences open import foundation-core.fibers-of-maps open import foundation-core.function-types open import foundation-core.functoriality-dependent-pair-types open import foundation-core.identity-types open import foundation-core.precomposition-functions open import foundation-core.sets
Idea
The axiom of choice¶ asserts that for every family of
inhabited types B
indexed by a
set A
, the type of sections of that family
(x : A) → B x
is inhabited.
Definition
The axiom of choice restricted to sets
AC-Set : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) AC-Set l1 l2 = (A : Set l1) (B : type-Set A → Set l2) → ((x : type-Set A) → is-inhabited (type-Set (B x))) → is-inhabited ((x : type-Set A) → type-Set (B x))
The axiom of choice
AC-0 : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) AC-0 l1 l2 = (A : Set l1) (B : type-Set A → UU l2) → ((x : type-Set A) → is-inhabited (B x)) → is-inhabited ((x : type-Set A) → B x)
Properties
Every type is set-projective if and only if the axiom of choice holds
is-set-projective-AC-0 : {l1 l2 l3 : Level} → AC-0 l2 (l1 ⊔ l2) → (X : UU l3) → is-set-projective l1 l2 X is-set-projective-AC-0 ac X A B f h = map-trunc-Prop ( ( map-Σ ( λ g → ((map-surjection f) ∘ g) = h) ( precomp h A) ( λ s H → htpy-postcomp X H h)) ∘ ( section-is-split-surjective (map-surjection f))) ( ac B (fiber (map-surjection f)) (is-surjective-map-surjection f)) AC-0-is-set-projective : {l1 l2 : Level} → ({l : Level} (X : UU l) → is-set-projective (l1 ⊔ l2) l1 X) → AC-0 l1 l2 AC-0-is-set-projective H A B K = map-trunc-Prop ( map-equiv (equiv-Π-section-pr1 {B = B}) ∘ tot (λ g → htpy-eq)) ( H ( type-Set A) ( Σ (type-Set A) B) ( A) ( pr1 , (λ a → map-trunc-Prop (map-inv-fiber-pr1 B a) (K a))) ( id))
Recent changes
- 2024-04-11. Fredrik Bakke and Egbert Rijke. Propositional operations (#1008).
- 2024-02-06. Egbert Rijke and Fredrik Bakke. Refactor files about identity types and homotopies (#1014).
- 2024-01-25. Fredrik Bakke. Basic properties of orthogonal maps (#979).
- 2023-12-21. Fredrik Bakke. Action on homotopies of functions (#973).
- 2023-11-24. Egbert Rijke. Refactor precomposition (#937).