I am pro-choice. I even have a T-shirt that says so. In type theory the axiom of choice is a logical consequence; it states that for every type A and B and every relation R between A and B that if ∀ a:A. ∃ b:B. R a b then ∃ f:A ⇒ B. ∀ a:A. R a (f a).
In set theory the axiom of choice has some unfortunately consequences such as the fact that one can well-order the real numbers. I used to grudgingly accept such consequences. It was better than not having choice. However intensional type theory does not imply these consequences. Intensional type theory distinguishes the intensional axiom of choice from the extensional axiom of choice.
What is stated above is the intensional axiom of choice. It is equivalent to saying that every surjective function has a right inverse. The extensional axiom of choice states that if (A, ≍A) and (B, ≍B) are setiods (a type and equivalence relation on that type), and R is a relation on A and B respecting the equivalence relations, then if ∀ a:A. ∃ b:B. R a b then ∃ f:A ⇒ B. ∀ a:A. R a (f a). Furthermore, f will respect the equivalence relations. The extensional axiom of choice is equivalent to saying that for every surjective extensional function there exists a right inverse that is also extensional.
This stronger, extensional axiom of choice is not derivable in intensional type theory. In fact, the extensional axiom of choice implies the law of the excluded middle. The key difference between set theory and type theory is that in set theory one can form quotient sets for arbitrary equivalence relations. In intensional type theory, one cannot form quotient types. If one could form quotient types, then one could reduce an extensional relation to an intensional relation on quotient types. Then one could use the intensional axiom of choice to get the extensional choice function.
I am pleased with this result. Type theory gives me the axiom of choice, but by throwing away the ability to make quotient types, the axiom of choice doesn’t produce the pathologies that it produces in set theory.
For more information see EM + EXT- + ACint is Equivalent to ACext by Jesper Carlström.