A principle that is analytically true under constructive semantics does not import classical logic principles such as Excluded Middle

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 existe