Recall Freyd's model of $ZF +\neg AC$ (as recounted in MacLane and Moerdijk's book Sheaves in Geometry and Logic): it arises as the Fourman interpretation of the topos of sheaves on a particular countable site, with underlying category $A$ as follows:

- Objects: natural numbers, coded as finite sets $\{1,2,\ldots,n\}$,
- Arrows: retracts $n \to m$ for $n \ge m$ and none otherwise.

We take the double-negation topology and consider $Sh_{\neg\neg}(A)$. The sequence of objects $F_n = A(-,n)^+$, $n\in \mathbb{N}$ (here ${}^+$ denotes sheafification) is such that

$F_n \to 1$ is an epi,

$F_n \hookrightarrow P(\coprod_\mathbb{N} 1) = P(\hat{\mathbb{N}})$ (so these are 'sets of subsets' of $\hat{\mathbb{N}}$, the NNO of $Sh_{\neg\neg}(A)$)

$\prod_\mathbb{N} F_n = 0$, the initial object

Thus the epi $\coprod_\mathbb{N} F_n \to \hat{\mathbb{N}}$ is a counterexample to the internal axiom of choice, and hence $AC$ fails in the Fourman interpretation (alternatively, let me just mention the words 'stack semantics' at this point, and maybe Mike Shulman will magically appear)

What I would like to know is, what do these 'sets' $F_n$ look like?

I am constructing a topos over $Set$ where these are the sets in Freyd's model, and would like to consider elements of the $F_n$. I could alternatively work over $Sh_{\neg\neg}(A)$ instead, but that is one step removed from the set theory.

Clearly I can consider $Hom(1,F_n)$, but my intuition tells be that this is not what the set corresponding to $F_n$ is in the Fourman interpretation/stack semantics.

Here's an idea, espressed in very rough terms. Consider generalised elements of the $F_n$, namely maps $A \to F_n$. We might as well only consider elements of the form $\coprod_{m\in S} F_m \to F_n$, for some $S \subset \mathbb{N}$ for various reasons I won't explain (I'm working a bit from intuition here - there are probably watertight reasons one could come up with). But recall that there are no maps $m\to n$ if $ m \lt n$, so one can roughly see that really there should only be generalised elements $\coprod_{m\in S} F_m \to F_n$ where $S \subset \mathbb{N} \cap [n,\infty)$.

And then a generalised element of $\prod_\mathbb{N} F_n$ should be a map $$ \coprod_{m\in S} F_m \to \prod_\mathbb{N} F_n $$ but the projection to $F_n$ ensures that $S \subset \mathbb{N} \cap [n,\infty)$ for all $n$, hence there are no such maps, and so $\prod_\mathbb{N} F_n$ has no elements.

So morally, $F_n$ looks like the subset of $P\mathbb{N}$ consisting of all sets with all elements greater than or equal to $n$. But I can't prove this, or give an explanation more rigorous than the above.