Global choice

module foundation.global-choice where

Imports

open import foundation.functoriality-propositional-truncation
open import foundation.hilberts-epsilon-operators

open import foundation-core.dependent-pair-types
open import foundation-core.equivalences
open import foundation-core.negation
open import foundation-core.universe-levels

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

Idea

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.

Definition

The global choice principle

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

Properties

The global choice principle is inconsistent in `agda-unimath`

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