Here's a mix of heuristic and precise questions as I try to grapple with topos theory.


I try to think of topoi as two notions of "$1$" being glued at the hip. One is the "building block" $1$, generating the naturals, the ordinals, the cardinals... with all its usual arithmetic properties. This generates the set theory of a topos.


The other is the "all-encompassing" $1$, the highest truth value, the top element of a Heyting/Boolean algebra, whose subobjects form the algebra of truth values in the topos. This generates the logic of a topos.


Hence the set-theoretical properties (existence of an NNO, choice, CH, large cardinals...) happen "above $1$" and the logical properties (being Boolean, two-valued, well-pointed...) happen "below $1$" (whatever this means, this is just my heuristic).


Now Grothendieck topoi are defined as sheaf topoi with values in a certain well-pointed topos, namely $\textbf{Set}$. I can construct topoi that are not Grothendieck by taking a $\textbf{Set}$-like topos that is not $\textbf{Set}$, for example $\textbf{FinSet}$, and then considering sheaves valued in it. My first question is: are all topoi generated like this? **Is every topos equivalent to a topos of sheaves on a site** (its logic) **with values a well-pointed topos** (its set theory)**?**


Taking the functor $(-)^1$ of global elements seems to suggest the affirmative, as it is a logical functor to its image $\mathcal{I}$, which is well-pointed. Then the topos is, I assume, equivalent to the $\mathcal{I}$-valued sheaves on its Heyting algebra.


My second suspicion was that the logic and the set theory of a topos are independent of each other, but upon reviewing forcing, this doesn't seem to be the case. For example, following Mac Lane and Moerdijk, I can start with $\textbf{Set}$, value presheaves on a forcing poset $P$ in it ($\widehat{P}$), make it Boolean ($\widehat{P}\_{\neg\neg}$) and mod out an ultrafilter ($\widehat{P}\_{\neg\neg}/\mathcal{U}$). But then I've changed the set theory of a topos by only tinkering with its logic. In this light, forcing seems really unexpected and counterintuitive, by creating an interplay between what's happening "above $1$" and "below $1$". [I suppose this is exactly what the forcing theorem in material set theory says, though.] So my second question is: **To what extent does forcing measure the interdependence of the logic and the set theory of a topos? Is there a theorem describing this?**


It also surprises me that the two constructions $(-)^1$ and $/\mathcal{U}$ to collapse a topos to a well-pointed one don't coincide. For example, $\textbf{Set} \cong (\widehat{P}\_{\neg\neg})^1$ and $\widehat{P}\_{\neg\neg}/\mathcal{U}$ generally differ. Is there a deep reason for this? Is it perhaps because the ultrafilter-quotient construction is not as well-behaved and purely logical as I think?



Is every topos a sheaf topos with values in a well-pointed one?
A solution to your first question is given in "Sketches of an Elephant" by Johnstone, Example A4.4.2(d). If a topos $\mathcal{E}$ is the topos of sheaves on some internal site in a topos $\mathcal{S}$, then there is a natural geometric morphism $p : \mathcal{E} \to \mathcal{S}$. It turns out that there are toposes that do not admit geometric morphisms to Boolean toposes whatsoever. Two examples given by Johnstone are the effective topos and the topos of triples $(A,B,f)$ where $A$ is a set, $B$ is a finite set, and $f : A \to B$ is a function.


So these toposes cannot be written as a topos of sheaves over a Boolean topos (so also not over a well-pointed topos, because well-pointed toposes are Boolean).


Below is the argument that a geometric morphism $p : \mathcal{E} \to \mathcal{S}$ does not exist, for $\mathcal{E}$ the topos of triples $(A,B,f)$ as above and $\mathcal{S}$ a Boolean topos. I follow the Elephant, Example A4.5.24. Because subtoposes of Boolean toposes are again Boolean, we can assume that $p$ is surjective, so $p^\*$ is faithful. Further, in $\mathcal{S}$ all objects are decidable, i.e. the diagonal embeddings $X \to X \times X$ have a complement. So the same holds for objects of the form $(A,B,f) = p^\*(X)$. This condition implies that $f$ is injective, and as a result both $A$ and $B$ are finite. We conclude that there are only finitely many morphisms $p^\*(X) \to p^\*(Y)$, and because $p^\*$ is faithful, it follows that there are only finitely many morphisms $X \to Y$, for $X,Y$ arbitrary. However, for $(A,1,f)$ with $A$ infinite, we get that there are infinitely many morphisms $1 \to p\_\*(A)$, so this gives a contradiction.


