Inspired by the question here, I have been trying to understand the sheaf-theoretic approach to forcing, as in MacLane–Moerdijk's book "Sheaves in geometry and logic", Chapter VI.

A general comment is that sheaf-theoretic methods do not a priori produce "material set theories". Here "material set theory" refers to set theory axiomatized on the element-of relation $\in$, as usually done, in ZFC. Rather, they produce "structural set theories", where "structural set theory" refers to set theory axiomatized on sets and morphisms between them, as in the elementary theory of the category of sets ETCS. I will always add a collection (equivalently, replacement) axiom to ETCS; let's denote it ETCSR for brevity. Then Shulman in Comparing material and structural set theories shows that the theories ZFC and ETCSR are "equivalent" (see Corollary 9.5) in the sense that one can go back and forth between models of these theories. From ZFC to ETCSR, one simply takes the category of sets; in the converse direction, one builds the sets of ZFC in terms of well-founded extensional trees (modeling the "element-of" relation) labeled by (structural) sets.

So for this question, I will work in the setting of structural set theory throughout.

There are different ways to formulate the data required to build a forcing extension. One economic way is to start with an extremally disconnected profinite set $S$, and a point $s\in S$. (The partially ordered set is then given by the open and closed subsets of $S$, ordered by inclusion.) One can endow the category of open and closed subsets $U\subset S$ with the "double-negation topology", where a cover is given by a family $\{U_i\subset U\}_i$ such that $\bigcup_i U_i\subset U$ is dense. Let $\mathrm{Sh}_{\neg\neg}(S)$ denote the category of sheaves on the poset of open and closed subsets of $S$ with respect to *this* topology.

Then $\mathrm{Sh}_{\neg\neg}(S)$ is a boolean (Grothendieck) topos satisfying the axiom of choice, but it is not yet a model of ETCSR. But with our choice of $s\in S$, we can form the ($2$-categorical) colimit
$$\varinjlim_{U\ni s} \mathrm{Sh}_{\neg\neg}(U)$$
called the filter-quotient construction by MacLane–Moerdijk. I'm highly tempted to believe that this is a model of ETCSR — something like this seems to be suggested by the discussions of forcing in terms of sheaf theory — but have not checked it. (See my answer here for a sketch that it is well-pointed. **Edit:** I see that well-pointedness is also Exercise 7 of Chapter VI in MacLane–Moerdijk.)

Questions:

- Is it true that $\varinjlim_{U\ni s} \mathrm{Sh}_{\neg\neg}(U)$ is a model of ETCSR?
- If the answer to 1) is Yes, how does this relate to forcing?

Note that in usual presentations of forcing, if one wants to actually build a new model of ZFC, one has to first choose a countable base model $M$. This does not seem to be necessary here, but maybe this is just a sign that all of this does not really work this way.

Here is another confusion, again on the premise that the answer to 1) is Yes (so probably premature). An example of an extremally disconnected profinite set $S$ is the Stone-Cech compactification of a discrete set $S_0$. In that case, forcing is not supposed to produce new models. On the other hand, $\mathrm{Sh}_{\neg\neg}(S)=\mathrm{Sh}(S_0)=\prod_{S_0} \mathrm{Set}$, and if $s$ is a non-principal ultrafilter on $S_0$, then $\varinjlim_{U\ni s} \mathrm{Sh}_{\neg\neg}(U)$ is exactly an ultraproduct of $\mathrm{Set}$ – which may have very similar properties to $\mathrm{Set}$, but is not $\mathrm{Set}$ itself. What is going on?

13more comments