Toposophy vs Set theoretical multiverse philosophy

Johnstones classic topos theory book talks at some length in its introduction about how category theory/topos theory suggest that we view the 'universe' in which mathematics takes place as consisting of 'dynamic sets'.

This is motivated in part by the fact that any topos can formulate an internal logic using its objects and arrows that enables it to make 'quasi-set theoretical statements' about its objects -- for example, he points out that the truth object of a topos allows us to convert the comprehension axiom into an elementary statement about adjoint functors. Johnstone claims that this, together with many other nice facts about topoi, lead the budding toposopher to view an arbitrary topos as the correct place to formulate mathematics instead of a fixed universe of sets together with some axioms.

In his own words:

What, then, is the topos-theoretic outlook? Briefly, it consists in rejection of the idea that there is a fixed universe of "constant" sets within which mathematics can and should be developed, and the regognition that a notion of 'variable structure' may be more convieniently handled within a universe of 'continuously variable' sets than by the method, traditional since the rise of abstract set theory, of considering separately a domain of variation (i.e. a 'topological space') and a succession of constant structures attached to the points of its domain.

On the other hand, we have the set-theoretic multiverse philosophy put forward and explored by Hamkins which argues that the method of forcing in set theory suggests we view the background on which mathematics takes place as a multiverse of universes of sets, each with its own internal structural properties -- he also suggests here that the multiverse view de-emphasizes structural properties of individual universes, as opposed to a universe-based view which might suggest that we explore properties of individual highly structured universes.

In his own words:

The multiverse view in set theory is a philosophical position offered in contrast to the Universe view, an orthodox position, which asserts that there is a unique background set-theoretic context or universe in which all our mathematical activity takes place. (...) A paradox for the universe view, which I mention in the slides to which you link, is that the most powerful set-theoretic tools that have informed a half-century of research in set theory are most naturally understood as methods of constructing alternative set-theoretic universes. (...) The multiverse view takes these diverse models seriously, holding that there are diverse incompatible concepts of set, each giving rise to a set-theoretic universe in which they are instantiated. The set-theoretic tools provide a means of modifying any given concept of set to a closely related concept of set, whose resulting universes can be fruitfully compared in a single mathematical context.

I am more familiar with topoi and two-dimensional/inner category theory than with forcing and related multiversal notions, but these two views seem quite similar in that they suggest many different possible places for 'ordinary' mathematics to be formulated, with consequences for each choice of location. My question is:

What is the relationship between a toposophers view of mathematics and a set-theoretical multiverse philosophers view? Has there been any work done on the relationship between the two?

For example, could each possible universe be cast as a topos with some additional structure dependent on the axioms underpinning the universe or vice verse, at least up to a canonical isomorphism or equivalence?

Here I transcribe some relevant comments made below:

Noah Schweber suggests and Sridhar Ramesh confirms that if you take a model of ZF and construct a topos from it, you can recover the ZF model from the topos, by first recovering the ordinals (as the structures the topos considers to be well-ordered), and then carrying out the construction of the cumulative hierarchy relative to those ordinals and the toposes' notion of power objects.

Sridhar also points out that all the forcing constructions of set theory have very direct topos theoretic analogues. Forcing over a partial order in the traditional sense is the same as constructing the presheaf topos over that partial order and then passing through the double negation transformation to recover a Boolean topos rather than an intuitionistic one, as well as the fact that toposes are agnostic to distinctions like between ZF vs. ZF - Foundation + Aczel's Antifoundation Axiom, or the like. You can just as well recover from a ZF topos a model of ZF - Foundation + Aczel's Antifoundation Axiom, if you like, by constructing (essentially) the terminal coalgebra for the powerset functor instead of the initial algebra, or such things. Toposes only care about sets up to cardinality, and do not care about any canonical inner structure imposed upon them (toposes are "structural set theory", blind to "material set theory" distinctions).

It is also pointed out that you can analogously construct a model of ZF-Foundation+AAA from a model of ZF, and so on, but that given a model of some arbitrary material set theory, not presumed off the bat to be specifically a model of ZF or a model of Antifoundational ZF, you can tell which one the model is actually of (even though you can extract a corresponding model of the other in either case). Whereas with a topos generated from these, there's no notion of whether it's a Foundation topos or an Antifoundation topos; it's the same topos either way.

• For a technical acount of how to go back and forth between toposes and model of ZF I recommand reading MIke shulman's paper "arxiv.org/abs/1004.3802". The short answer is that these two point of view are indeed very similar up to small techincal difference: the difference between mateial/structural set theory mentioned in previous comment, toposes allows for intuitionistic logic, and toposes comes without the unbounded replacement axiom (which make then quite weaker than ZF in terms of proof theoretic strength) – Simon Henry Dec 18 '18 at 21:03
• @SridharRamesh I’m always confused when you category guys seem to blur the distinction between a mathematical structure and the theory it satisfies. What’s going on with that? – Monroe Eskew Dec 19 '18 at 7:34
• @SridharRamesh- What informs this use of terminology? It’s against the mainstream usage in logic. A theory is a collection of sentences in a language. A structure is a collection of things with functions and relations. The satisfaction of sentences by a structure is defined and we ask whether the structure satisfies a theory. Sometimes such questions are hard. There are often many nonisomorphic structures satisfying a given theory, and often many interpretations of the language in a structure (this is relevant in, for example, rigidity). These are just not the same kind of thing. – Monroe Eskew Dec 19 '18 at 20:37
• Furthermore, provability commutes with logical operators only for complete theories, which are usually not computable. And complete theories cannot be identified with structures because there are often many structures satisfying complete theories, many interpretations of a theory in a structure, etc. – Monroe Eskew Dec 19 '18 at 20:42
• Please explain why truth = provability in ZF In one of the toposes you defined. I already pointed out some problem with the definable-sets category, and Dorais seemed to agree there was something wrong, and then you said the objects could be chosen differently. So I’m guessing the idea is some kind of syntactic trick going on to achieve the truth values you want (having to do with the fact that the objects are formulas?), which seemed to be the main point. What’s the argument? – Monroe Eskew Dec 25 '18 at 6:31