open import 1Lab.Prelude

open import Data.Bool
open import Data.Dec

module 1Lab.Counterexamples.GlobalChoice where


# Global choice is inconsistent with univalence🔗

The principle of global choice says that we have a function for any type 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 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 which is equivalent to also fails:

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