How important is global choice (a la Lean, HOL Light, Isabelle/HOL) practically?

Question

Choice is indispensable for much of modern classical mathematics. Therefore, most proof assistants offer it as part of their standard library. The most powerful version is sometimes called global choice or Hilbert's choice operator. This I believe is the version used by Lean, HOL-Light, and Isabelle/HOL, and they use it liberally. In particular, in Lean it is given by:

axiom choice {α : Sort*} : nonempty α → α

However, in some ways, global choice is maybe a bit too strong. It isn't compatible with univalent foundations and it leads to a strange situation where one can define named functions which are not well-defined such as the function mapping a vector space to its basis.

Instead there are two other forms of choice which are more reasonable, unique choice and the axiom of choice.

By unique choice (UC), I mean the version which is comparable to Lean's choice operator, but requires a unique element to choose from. I believe it is also called Church's iota operator.

axiom unique_choice {α : Sort*} : nonempty α → subsingleton α → α

This still allows us to define functions by their properties, as long as we can show only one such function exists. (In many logics, this follows from other axioms.)

By the Axiom of Choice (AC) I mean something like this:

axiom axiom_of_choice : ∀ (A B : Type) (R : A → B → Prop),
  (∀ x : A, ∃ y : B, R x y) -> ∃ f : A → B, (∀ x : A, R x (f x))

I may also need to allow B(x) to depend on x : A. (Also, this is the version where we assume all types are sets, in the HoTT sense. More generally, we would restrict A to be a set.)

My question is if it is practical to replace global choice with unique choice and the axiom of choice?

For example:

1. Would it be fairly routine to replace global choice in Lean's mathlib, HOL-Light's library, or Isabelle's AFP with the axiom of choice and unique choice?
2. Do practitioners in Coq and other systems where they are more careful with axioms find it easy to do modern classical mathematics with just UC and AC?

For clarification, my question is not about

• the pure logical strength of global choice: I don't know the specifics, but I assume there is something that can be proved with global choice and can't with AC + UC. If so, I'm also assuming it isn't particularly mathematically relevant or meaningful. Of course, if I'm mistaken and there is a theorem commonly used in mathlib, AFP or HOL-Light that doesn't have a simple AC + UC provable alternative, I'd love to hear it.
• pedantry: I might be not stating UC or AC in exactly the way I need or there may be an extra axiom that is needed to go with AC + UC to replace global choice. If so, I'd love to hear it, but please also assume my question assumes that "correct" formulation as well. Nonetheless, I'd only like axioms which roughly follow from both DTT + global-choice and DTT + UA + HIT + AC. (I say roughly, since the my version of AC assumes that all types are sets, whereas a univalent version would be more careful to specify sets explicitly.)
• constructive math: I'm not asking about removing all choice, just global choice (and replacing it with AC + UC).

---

My motivation for this question is trying to understand how well modern developments of classical formal mathematics can be fit with univalent foundations as in this question. The difference between how one states the axiom of choice seems to be one of the largest differences between say Lean and univalent foundations (but obviously not the only one).

Answer 1

I think the main practical use of global choice is to be able to make definitions that depend on choice without having to wrap them inside nonempty. For example, the definition of algebraic closure in mathlib is currently made up of the following four definitions. I think the advantage of global choice over non-global choice is mainly just a matter of convenience.

def algebraic_closure (k : Type u) [field k] : Type u :=

instance (k : Type u) [field k] : field (algebraic_closure k) :=

instance (k : Type u) [field k] {R : Type*} [comm_semiring R] [alg : algebra R k] :
  algebra R (algebraic_closure k) :=

instance (k : Type u) [field k] : is_alg_closure k (algebraic_closure k) :=

Your version of choice, axiom_of_choice is equivalent another version which I prefer ∀ {ι : Type} {α : ι → Type}, nonempty (Π (i : ι), nonempty (α i) → α i).

axiom axiom_of_choice : ∀ (A B : Type) (R : A → B → Prop),
  (∀ x : A, ∃ y : B, R x y) -> ∃ f : A → B, (∀ x : A, R x (f x))


example {ι : Type} {α : ι → Type} : nonempty (Π (i : ι), nonempty (α i) → α i) :=
let ⟨f, hf⟩ := axiom_of_choice {i : ι // nonempty (α i)} (sigma α) (λ a b, b.1 = a)
  (λ i, let ⟨i2⟩ := i.2 in ⟨⟨i.1, i2⟩, rfl⟩) in
⟨λ i hi, 
  have h : (f ⟨i, hi⟩).1 = i, from hf ⟨i, hi⟩,
  eq.rec_on h (f ⟨i, hi⟩).2⟩


axiom axiom_of_choice2 {ι : Type} {α : ι → Type} : nonempty (Π (i : ι), nonempty (α i) → α i)

example (A B : Type) (R : A → B → Prop)
  (h : ∀ x : A, ∃ y : B, R x y) : ∃ f : A → B, (∀ x : A, R x (f x)) :=
let ⟨f⟩ := @axiom_of_choice2 A (λ a, {b : B // R a b}) in
⟨λ a, (f a (let ⟨b, hb⟩ := h a in ⟨⟨b, hb⟩⟩)).1, 
 λ a, (f a (let ⟨b, hb⟩ := h a in ⟨⟨b, hb⟩⟩)).2⟩

Without global choice I believe it's still possible to prove the mere existence of an algebraic closure. This would be more unpleasant to state however. The definition would look something like this.

structure algebraic_closure (K : Type u) [field K] : Type (u+1) :=
( carrier : Type u )
[ i₁ : field carrier ]
[ i₂ : algebra K carrier ]
[ i₃ : is_alg_closure K carrier ]

lemma exists_algebraic_closure {K : Type u} [field K] : 
  nonempty (algebraic_closure K)

This would be much less convenient to use, but it wouldn't significantly change the maths that is possible to prove. It is merely a matter of convenience.

A proposal to get around the issue of convenience would be to introduce some sort of special universal quantifier that behaved in a way similar to how universe polymorphism currently works in Lean 3. If we use the notation ∀2 for this quantifier then the axiom of choice would be stated as simply

axiom choice : ∀2 {ι : Type}, ∀2 {α : ι → Type}, nonempty (Π (i : ι), nonempty (α i) → α i)

ι must be a set for this to be consistent with univalence.

The difference between ∀2 and ∀ is that ∀2 should only appear at the beginning of a declaration, and never in the middle of a term. So for example, something like (∀2 x, B x) -> A is not allowed. Also, anything containing a ∀2 is not a type. This axiom can be thought of as an axiom schema saying that for any type α, the type nonempty α -> α is inhabited without saying that the type ∀2{α : Type}, nonempty α -> α is inhabited.

Any declaration starting with a ∀2 should only be applied to term which do not contain any variables in the context other than those introduced with a λ2.

The reason I say this is something like how universe polymorphism works in Lean 3 is that a universe polymorphic definition like list.length in some sense quantifies over universe. i.e

def list.length {v} {α : Type v} : list α -> nat

could be thought of as having some special universe quantifier, ∀u at the beginning

def list.length : ∀u v, ∀ α : Type v, list α -> nat

This ∀u can only appear at the very beginning of a declaration. It is not valid in Lean to have a universe polymorphic hypothesis to a theorem. example (h : ∀u v, A : Type v, nat) : nat is not valid for example.

Using this axiom schema version of choice, it should be possible to prove all theorem schema or definition schema about the algebraic closure in a similar way to how they are currently stated in mathlib.

def algebraic_closure : ∀2 (k : Type u) [field k], Type u 

etc.

This statement of choice should be compatible with univalence because the usual proof of false from global choice is the following. We're assuming choice : ∀2 (α : Type}, nonempty α → α. This is implied by (but not equivalent to) the version above ∀2 {ι : Type}, ∀2 {α : ι → Type}, nonempty (Π (i : ι), nonempty (α i) → α i), because it is cleaner to prove the contradiction this way.

If swap is the path bool = bool corresponding to the equivalence that swaps the two elements of bool then it is false that

choice bool _ = cast swap (choice bool _)

However, using the recursor for equality we can prove this. The motive is will be λ (A : Type) (h : A = bool), choice A _ = cast h (choice bool). This is true when applied to bool and eq.refl _, but false when applied to bool and swap.

This proof doesn't work with the ∀2 version of choice however, because in the motive for the induction on equality, we apply choice to a bound variable.

Sorry if this is not the best explanation, I'm not that experienced in explaining type theory in the normal language and presentation. I think about type theory in terms of Lean, not the way it is usually presented in type theory papers.