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)