Global choice

Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides and Elisabeth Bonnevier.

Created on 2022-02-08.
Last modified on 2023-09-14.

module where
open import foundation.dependent-pair-types
open import foundation.functoriality-propositional-truncation
open import foundation.hilberts-epsilon-operators
open import foundation.universe-levels

open import foundation-core.equivalences
open import foundation-core.negation

open import univalent-combinatorics.2-element-types
open import univalent-combinatorics.standard-finite-types


Global choice is the principle that there is a map from type-trunc-Prop A back into A, for any type A. Here, we say that a type A satisfies global choice if there is such a map.


The global choice principle

Global-Choice : (l : Level)  UU (lsuc l)
Global-Choice l = (A : UU l)  ε-operator-Hilbert A


The global choice principle is inconsistent in agda-unimath

  no-global-choice :
    {l : Level}  ¬ (Global-Choice l)
  no-global-choice f =
      ( λ X 
        f (pr1 X) (map-trunc-Prop  e  map-equiv e (zero-Fin 1)) (pr2 X)))

Recent changes