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)