A very satisfying answer to my recent question on this list has been given to me by Andreas Blass. Since \Delta : Set -> Psh(G) is logical there is no way of defining a generic family of finite objects in the language of higher order arithmetic since every such family would be of the form \Delta(u). That such a family can't be generic is shown already by the argument in my mail. Moreover, as he pointed out and I also observed, although A -> I is a family of finite sets iff \forall i:I.\exists! n:N. A_i \cong K_n there will in general be no external choice function providing such an n:N for i:I although internally by AUC there exists a unique such choice function. After all this is no suprise since the representable object of Psh(G) has global support but no global element (unless G is trivial). Thomas