Suppose we want to prove that (classical!) $\mathsf{ZF}$ does not prove, say, “for every infinite set $A \subseteq \{0,1\}^{\mathbb{N}}$ there exists an injection $\mathbb{N} \to A$” (I take this example as about the simplest possible example of a refutation of Choice). The approach originating in Cohen's work proceeds roughly as follows (see Jech, Set Theory: Third Millennium Edition, example 15.52 for details):
Step 1. Choose a notion of forcing (here we will take partial functions $\mathbb{N}^2 \dashrightarrow \{0,1\}$ with finite domain, ordered by reverse extension), which in turn defines a complete Boolean algebra $\mathbf{B}$ (here the Boolean algebra of regular open sets of the product topology on $\{0,1\}^{\mathbb{N}^2}$), which in turn defines a Boolean-valued model $V^{\mathbf{B}}$ of $\mathsf{ZFC}$ (here, essentially, adding $\omega$ Cohen-generic elements of $\{0,1\}^{\mathbb{N}}$, precisely the $(a_n)$ where $a_n := a(n,—)$ is the slice of the generic function $a: \mathbb{N}^2 \to \{0,1\}$ inside $V^{\mathbf{B}}$ such that the truth value of $a(n,p)=i$ is given by the partial function $\{(n,p,i)\}$).
Step 2. Choose a group of permutations acting on the notion of forcing (and hence the Boolean algebra, and hence on the Boolean-valued model) of step 1, and a normal filter of subgroups of this group, and call “symmetric” the elements of the Boolean-valued model which are symmetric under a subgroup in the filter, and “hereditarily symmetric” those symmetric elements whose elements are themselves hereditarily symmetric: then the hereditarily symmetric elements will form a submodel $N$ of $V^{\mathbf{B}}$ which models $\mathsf{ZF}$ and, in general, not $\mathsf{ZFC}$. (Here we will take the group of permutations of $\mathbb{N}$ acting on finite partial functions $\mathbb{N}^2 \dashrightarrow \{0,1\}$ by permuting the first component of elements of $\mathbb{N}^2$, so effectively it permutes the $a_n$, and the normal filter of subgroups generated by fixators of finitely many elements.)
Now I would like to describe these two steps as operations on topoi. Let us restrict my goal to explaining why there is a Boolean topos in which the quoted sentence in the first paragraph of this question fails (i.e., forget about producing a model of $\mathsf{ZF}$, though a topos should probably be enough to get one of $\mathsf{Z}$).
I know how to describe step 1 in topos-theoretic terms: what we are doing is, essentially, taking the topos of $(\neg\neg)$-sheaves on the topos of sheaves on $\{0,1\}^{\mathbb{N}^2}$; more precisely, starting from a notion of forcing, we are taking its frame completion (here this will be the frame of open sets of $\{0,1\}^{\mathbb{N}^2}$), then taking the frame $\mathbf{B}$ of regular open subsets of that (i.e., the minimal dense sublocale, or “booleanization”) in order to keep classical logic, and we are dealing with the topos of sheaves on this locale. (The words “essentially” and “dealing with” are pushing some dust under the rug here: this question has more to say with the relation between $V^{\mathbf{B}}$ and the topos of sheaves on $\mathbf{B}$. But this is not what concerns me here, since as I just said I am willing to get less than a model of full $\mathsf{ZFC}$.)
What I want to understand, now, is step 2, i.e., how from the topos of sheaves on $\mathbf{B}$ (and a group of symmetries of it, and a normal filter of subgroups of that) we get a topos which “corresponds” to the symmetric submodel $N$ (putting the word “correspond” in quotes, because I'm not sure exactly what I should be asking for) and which refutes the quoted statement. So:
Question. How should we think of step 2 in the above approach, topos-theoretically? To what topos-theoretic construction does it correspond and what topos corresponding to $N$ does it construct? What functor (or geometric morphism) does this step 2 give between the topos of sheaves on $\mathbf{B}$ (corresponding to $V^{\mathbf{B}}$) and the topos corresponding to $N$?
I should note that there is an attempt to explain how to falsify Choice using a topos-theoretic construction in section VI.§4 of MacLane & Moerdijk's book Sheaves in Geometry and Logic, but it doesn't mention any connection with symmetric models, and I don't understand how it relates to the set-theoretic approach outlined above.
