Andrej Bauer writes about using alternatives to set-theories as foundations, (in particular homotopy type theory), in the article "Am I a constructive mathematician?" which contains the line "A world of mathematics may be a forcing extension of set theory, or a topos, or a pretopos, or a model of type theory, or any other structure within which it is possible to interpret the basic language of mathematics."
One viewpoint is that there isn't a one true set-theory but a set-theoretic multiverse. Might we not then in a similar vein say there is also a topos-theoretic multiverse, a homotopy-type-theoretic multiverse (a submultiverse of the type-theoretic multiverse?), and many other basic-language-of-mathematics-interpreting-structure multiverses that haven't been discovered.
Para-quoting Andrej Bauer again: "infinitely many worlds of mathematics ... visit them all, understand how they are related, and see what happens to his favorite subject as he moves between them" - this is where the Inter-Multiversal bit comes in. Which multiverse does Mochizuki's Inter-Universal fit into?
If a particular flavor of multiverse, say the set-theoretic multiverse, is formalized then perhaps one could vary that formalization to arrive at a multimultiverse for that flavor (as mentioned in comments in the above link), but what is the collective noun for a collection of different flavors of multiverses? A manifest of multiverses? Does the manifest of all multiverses constitute an omniverse?
-
Questions:
1) What other examples are there of "structures within which it is possible to interpret the basic language of mathematics"?
2) Do you actually need something like a transfer principle from non-standard analysis in order to make use of results from a different universe or multiverse, or can you theorize about collections of universes and multiverses and thereby learn things that will be of use for the particular universe that you are most interested in? i.e. what alternatives are there to transfer-principles?
