The attached screenshot, from Goldblatt's Topoi, shows at a glance the distinction between the constructive concept of inhabited set versus that of the classical nonempty set.
These definitions seem only equivalent if the axiom of excluded middle is assumed. However, in the absence of this axiom, the distinction seems fundamental (Why isn't this taught in the math curriculum?)
By analogy to Herrlich's Axiom of Choice which lists "disasters without choice", "disasters with choice" and "disasters either way", is there a published list of consequences of this difference?
In other words, which major results that rest on provably nonempty sets in classical logic cannot be proven to be inhabited sets without excluded middle?
By the way, at the end of Khamsi and Kirk's Introduction to metric spaces and fixed point theory the authors point out three variations on constructive mathematics developed by different mathematicians such as Brouwer and A Markov (Jr). It would be interesting then to also compare what effect these variations have on the emergent set theory.