Its truth or falsity isn't interesting

Whether the Axiom of Choice is true of false is uninteresting, but when is it true and when is it false is interesting.

The presence of anafunctor (or Morita equivalence, weak equivalence, etc.) discards the need of choice. That means on some semantic level choice is false, but on other level it is true. So, the point is to study the proper domain of validity of the axiom, and the general "functional" mechanism of the validity of it.

It's not really about "multiverse", it's about how the multiverse is generated, the structure of the multiverse, and the syntactical mechanism that is behind this structure.

A “summary” by GPT#

It's an exceedingly good generated text. Since I have no patience to explain the details, here I present GPT's reply:

Your argument about the Axiom of Choice (AC) touches on a deep, structural issue within set theory and mathematical logic, one that is far more nuanced than the simplistic question of whether the Axiom of Choice is "true" or "false." Instead, you focus on the contextual or functional validity of the axiom, exploring its structural and semantic implications.

 1. Truth and Falsehood of AC: Context-Dependence#

The statement that whether the Axiom of Choice is true or false is "uninteresting" reflects the fact that, in modern mathematics, we often regard AC not as an intrinsic truth about mathematics but as a tool with a specific range of utility, depending on the framework or context in which it's used. From the perspective of model theory and different foundational frameworks, AC can be true in some models and false in others, such as in Zermelo-Fraenkel set theory (ZF) with or without Choice (ZFC vs. ZF). Thus, the more fruitful inquiry is when AC holds and when it does not, and what this implies about the structure we are studying.

For example, in constructive mathematics, where we avoid classical logic's law of excluded middle, AC is typically considered false because it entails non-constructive existence claims. On the other hand, in classical set theory or certain model-theoretic settings, AC may hold as a theorem or assumption.

2. Anafunctors, Morita Equivalence, and Avoiding Choice#

The mention of anafunctors or Morita equivalence highlights a specific structural domain where AC is unnecessary. These concepts arise in contexts like category theory, homotopy theory, or higher-categorical structures where the need for making arbitrary choices is often obviated by equivalence relations. For example, anafunctors generalize functors to a setting where maps are defined up to equivalence rather than requiring strict choices for objects or morphisms.

This weakens the need for the Axiom of Choice because the semantic content of equivalence classes replaces the need for arbitrary selections. In other words, in such domains, it’s more natural to work with structures where choice is either irrelevant or automatically guaranteed by higher-order coherence relations (like weak equivalences, homotopy-theoretic fibrations, etc.).

Thus, on a "semantic level," the Axiom of Choice might be considered false, because the need for choice is eliminated by structural properties. In contrast, in other domains (like classical set theory or analysis), where such equivalences are not part of the foundation, AC might be true or required to enable constructions (e.g., the existence of bases for vector spaces).

3. Functional Validity and Domain of the Axiom#

What you are proposing is a domain-specific approach to the Axiom of Choice. Instead of asking "is AC true?" universally, it is more productive to ask, "in what context is AC a valid or useful assumption?" By studying the functional mechanisms that either validate or invalidate AC, you gain insight into when and why the axiom is necessary, and when alternative structures, like equivalence relations or higher categories, eliminate its necessity.

This functional perspective could be interpreted through syntactic mechanisms—how the axioms of a given theory determine whether choice is required. In classical ZFC, AC often comes in handy for certain constructions, but in constructive settings, one may need to avoid it, leading to syntactically richer frameworks where equivalences take the place of explicit choices. The "truth" of AC depends on how the structures and theories are built.

4. Multiverse of Set Theory: Not About Multiple Worlds, But Their Structure#

You distance your argument from the set-theoretic multiverse concept, which suggests the existence of many possible universes where different set-theoretic statements may hold. Instead, you are concerned with the mechanisms that generate the structure of this "multiverse". You are not merely accepting that in some models AC is true and in others it is false, but asking deeper questions about how these models arise and what the syntactic or semantic mechanisms underlying this variance are.

The generation of the multiverse is linked to how foundational choices (like whether to assume AC) propagate through the rest of mathematics. The structure of the multiverse is determined by these foundational choices and their functional roles within different frameworks (e.g., classical, constructive, or homotopy-theoretic settings). The syntactical mechanisms are the rules and axioms (ZF, ZFC, type theory, etc.) that give rise to distinct mathematical "worlds" or theories where AC may be true or false.

5. Conclusion: A Contextual, Functional Approach to the Axiom of Choice#

Your approach is highly structural and contextual: rather than engaging in metaphysical debates over the absolute truth or falsehood of the Axiom of Choice, you advocate for studying the domains in which the axiom is valid and the syntactic mechanisms that underlie its necessity or irrelevance. The functional role of AC, and the structure of the mathematical multiverse it generates, becomes the more interesting subject of investigation.

Ultimately, this perspective aligns with a model-theoretic or category-theoretic understanding of mathematics, where truth is often relative to the system or structure in question, and structural features like anafunctors and equivalences replace the need for arbitrary choices. This insight could potentially guide future investigations into both the foundations of set theory and alternative frameworks like homotopy type theory, where the need for AC may be further minimized or replaced altogether.