Axiom of Choice in Constructive Mathematics. Is it really an axiom?

Question

The status of the Axiom of Choice varies between different branches of Constructive Mathematics. For example, in Constructive Set Theory the Axiom of Choice is not accepted because it implies the law of excluded middle, but in Intuitionistic Type Theory the Axiom of Choice is a theorem that can be proved. Are there other branches of Constructive Mathematics in which the Axiom of Choice is really an axiom (I mean, it's assumed true but not provable)?

Answer 1

The version of the axiom of choice probable in intuitionist type theory bears only a formal resemblance to what set theorists think of as the axiom of choice. The issue is that one can’t really interpret the existential quantifier $\exists$ as $\sum$ in many cases when doing ordinary mathematics. $\DeclareMathOperator{refl}{refl}$

For instance, consider $\{x \in \{1\} \mid \exists y \in \mathbb{Z} (y^2 = x)\}$. How many elements does this set/type have?

In set theory, the answer should clearly be 1. But in type theory, if we interpret the above as $\sum (x : \{1\}) \sum (y : \mathbb{Z}) (y^2 = x)$, then the type has two distinct elements, $(1, (1, \refl_1))$ and $(1, (-1, \refl_1))$. This is why propositional truncation types are necessary.

The same thing happens in a much more dramatic fashion when one tries to develop, for instance, the Dedekind reals.

The solution is to use propositional truncation or, more generally, to allow quotient types (or other forms of higher inductive types). Then, one can interpret $\exists$ in a manner consistent with ordinary mathematics. When one does so, the axiom of choice is not provable.

That said, many versions of constructive mathematics take weak versions of choice as axioms, including countable choice, dependent choice, and COSHEP (category of sets has enough projectives).