I'm interested in dream mathematics (https://ncatlab.org/nlab/show/dream+mathematics) as a foundation of "synthetic measure theory" in a similar vein as synthetic differential geometry, but I'm unclear on its relationship to ordinary mathematics, particularly as expressed through topos theory.

As far as I understand it, any model $V$ of ZFC with enough large cardinals allows for the construction of a model $W$ for dream mathematics by repeatedly applying the "definable subset" functor to the reals, as described here: https://en.wikipedia.org/wiki/L(R). This structure fulfills the axioms of ZF as well as determinacy, and thus has to be a topos.

**I'd like to use internal reasoning within the topos of $W$ to derive results and export them to $V$ with some caveat like "these results hold for all definable subsets".**

However, first I'd like to understand the relationship between $V$ and $W$ better. In particular, it seems that the embedding functor from $W$ to $V$ is neither a geometric nor a logical morphism of topoi.

Furthermore, I don't understand how to get from the topos structure of $V$ to that of $W$ since they have the same subobject classifier but different power object functors. For this to make any sense, the number of functions from the real numbers to the subobject classifier in $W$ has to be a subset of the functions in $V$, so the embedding of $W$ into $V$ cannot be full.

My questions are:

Is there a clear or clearer description of which functions in $V$ make it over into $W$?

Are there any transfer rules between $V$ and $W$ like those between models of synthetic differential geometry and normal differential geometry? Alternatively, are there any classes of preserved sentences, similar to the situation between nonstandard analysis and normal analysis?

More generally, what is the categorical relationship between $V$ and $W$?

full. $\endgroup$somemodel of ZF+DC+AD, then infinitely many Woodin cardinals suffices. $\endgroup$3more comments