>>10848796>what problem do people have the the AoC? what is wrong with it?This is a common misunderstanding among math folks not versed into logic: the problem is not the axiom of choice alone, the real issue is the axiom of choice in presence of classical logic.
For instance, in Martin-Löf type theory axiom of choice holds by construction, and can be given a trivial computational meaning. In ??-calculus, you can get computational classical logic but axiom of choice is broken. Providing a reasonable computational account of classical logic + choice has been the center of research for years, to no avail (see e.g. Krivine's classical realizability). Weaker versions are OK, like countable or dependent choice though.
