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 $\Vert A\Vert \to A$ for any type $A\text{.}$ 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 $\Vert A\Vert \to \neg \neg A\text{,}$ 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 ${\mathrm{LEM}}_{\infty }\text{,}$ which is equivalent to ${\mathrm{DNE}}_{\infty }\text{,}$ also fails:

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