module 1Lab.Counterexamples.GlobalChoice where

# Global choice is inconsistent with univalence🔗

The principle of **global choice** says that we have a
function
$∥A∥→A$
for any type
$A.$
We show that this is inconsistent with univalence.

Global-choice : Typeω Global-choice = ∀ {ℓ} (A : Type ℓ) → ∥ A ∥ → A module _ (global-choice : Global-choice) where

The idea will be to apply the global choice operator to a
*loop* of types, making it contradict itself: since the argument
to `global-choice`

is a proposition, we
should get the same answer at both endpoints, so picking a non-trivial
loop will yield a contradiction.

We pick the loop on `Bool`

that swaps the two
elements.

swap : Bool ≡ Bool swap = ua (not , not-is-equiv)

The type of booleans is inhabited, so we can apply global choice to it.

Bool-inhabited : ∥ Bool ∥ Bool-inhabited = inc false b : Bool b = global-choice Bool Bool-inhabited

Since `∥ swap i ∥`

is a
proposition, we get a loop on `Bool-inhabited`

over `swap`

.

irrelevant : PathP (λ i → ∥ swap i ∥) Bool-inhabited Bool-inhabited irrelevant = is-prop→pathp (λ _ → is-prop-∥-∥) Bool-inhabited Bool-inhabited

Hence `b`

negates to itself, which is a
contradiction.

b≡[swap]b : PathP (λ i → swap i) b b b≡[swap]b i = global-choice (swap i) (irrelevant i) b≡notb : b ≡ not b b≡notb = from-pathp⁻ b≡[swap]b ¬global-choice : ⊥ ¬global-choice = not-no-fixed b≡notb

## ∞-excluded middle is inconsistent with univalence🔗

As a corollary, we also get that the “naïve” statement of the law of excluded
middle, saying that *every* type is decidable, is inconsistent
with univalence.

First, since $∥A∥→¬¬A,$ we get that the naïve formulation of double negation elimination is false:

¬DNE∞ : (∀ {ℓ} (A : Type ℓ) → ¬ ¬ A → A) → ⊥ ¬DNE∞ dne∞ = ¬global-choice λ A a → dne∞ A (λ ¬A → ∥-∥-rec! ¬A a)

Thus $LEM_{∞},$ which is equivalent to $DNE_{∞},$ also fails:

¬LEM∞ : (∀ {ℓ} (A : Type ℓ) → Dec A) → ⊥ ¬LEM∞ lem∞ = ¬DNE∞ λ A ¬¬a → Dec-rec id (λ ¬a → absurd (¬¬a ¬a)) (lem∞ A)