 The fact that the Axiom of Choice implies Excluded Middle seems at first sight to be at variance with the fact that the former is often taken as a valid principle in systems of constructive mathematics governed by intuitionistic logic, e.g. Bishop’s  Constructive Analysis[16]   and Martin-Löf’s Constructive Type  Theory[17], in  which Excluded Middle is not affirmed. In Bishop’s words, “A choice function exists in constructive mathematics because a choice is implied by the very meaning of existence.” Thus, for example, the antecedent  \(\forall x \exists y \phi(x,y)\) of ACL, given a constructive construal, just means that we have a procedure which, applied to each \(x\), yields a \(y\) for which \(\phi(x, y)\). But this is precisely what is expressed by the consequent \(\exists f \forall x \phi(x,fx)\) of ACL.