  When discussing the role of classical set theory as a foundation for mathematics, one usually considers the theory ZFC, that is, the axiom system ZF plus the axiom of choice (AC). One might therefore wonder what is the status of the axiom of choice in intuitionistic settings. The question is particularly significant because at its first appearance the axiom of choice was often seen as controversial and highly non-constructive. In constructive contexts, however, one witnesses a peculiar phenomenon. The usual form of the axiom of choice is validated by theories of types such as Martin-Löf type theory, where the Curry-Howard correspondence holds (See Section 3.4  of the entry on  Constructive mathematics).  On the other hand, the assumption of the axiom of choice gives rise to instances of the excluded middle in extensional contexts, where a form of separation is also available. This is the case, for example, of constructive and intuitionistic ZF. (For the proof, see the supplementary document on Set-theoretic Principles Incompatible with Intuitionistic Logic.)  A proof of the incompatibility of AC with extensional set theories based on intuitionistic logic seems to have first appeared in (Diaconescu 1975) in a categorical context. Goodman and Myhill give an argument for set theories based on intuitionistic logic (Goodman and Myhill 1978). 