generic families of finite sets in toposes with nno ?

generic families of finite sets in toposes with nno ?

[Thomas Streicher]

I have the following question about finite objects in toposes with nno
where with ``finite'' I mean K-finite and with decidable equality.

It is well known that in every topos EE with nno N there exists a family
k : K -> N of finite sets such that for every family a : A -> I of finite sets
there exists an epi e : I ->> J and a map f : J -> N such that e^*a \cong f^*k.
Such a map k one may call a ``weakly generic family of finite sets''.
I would like to know whether there always exists a family  \pi : E -> U  of
finite sets which is "generic" in the sense that for every family a : A -> I
of finite sets there exists an  f : I -> U  with  f^*k' \cong a.

Already for Psh(G) with G a nontrivial finite group one cannot take the usual
weakly generic map  k = \succ \circ \add : N x N -> N  because the
representable object G = y(*) is finite but not isomorphic to n^*k for some
n : 1 -> N.
However, for arbitrary small cats C such a map \pi : E -> U  exist: take
for U(I) the set of presheaves on C/I valued in FinSet_iso and where u operates
by precomposing with (C/u)^\op. E(I) consists of pairs (F,x) where F is in U(I)
and x \in F(\id_I). (This is a variation of a construction in my paper
"Universes in Toposes" pp.9-10 albeit with FinSet instead of a Groth.universe).

However, it is not clear to me for the case of sheaf toposes. In realizability
toposes I think the usual k = \succ \circ \add : N x N -> N does work.

Anyway, I would like to know if anyone has considered the problem and whether
there is a "logical" (i.e. in the internal language) construction of a generic
family family \pi : E -> U for every topos with nno.

Thomas Streicher