Comment by jasperry
So if I understand the claim of this correctly (I'm a spectator of logic research and haven't tried to follow the proofs), there is a constructive version of AoC that is obviously true, but it's not the same as Zermelo's axiom because that one is extensional. Zermelo's axiom can be formulated in constructive mathematics but gives you things you don't want (like excluded middle.)
Is this close to a correct statement of the paper's result? Is all this agreed on today? Have there been any significant refinements?
That sounds about correct. The naïve interpretation of AC that interprets ∃ as Σ and ∀ as Π amounts to the trivial fact that Π distributes over Σ, which has little to do with any choice principle. If you instead interpret it in setoids, as Martin-Löf does, then the function you get should be extensional with respect to the relevant setoid structures, which is where the power of the axiom comes from.
The modern view on this is homotopy type theory, where types themselves are intrinsically seen as ∞-groupoids (a higher analogue of setoids) and ∃ is interpreted as a propositionally truncated Σ-type (see chapter 3 of the HoTT book). In this setting the axiom of choice says that for any set X, (∀ (x : X). ∥ P x ∥) → ∥ ∀ (x : X). P x ∥ (see section 3.8).
Note that from the perspective of homotopy type theory, Zermelo's axiom of choice is too strong: it is equivalent to global choice (for all types A, ∥ A ∥ → A), which is inconsistent with univalence.