answer by Blass: generic family

answer by Blass: generic family

[Thomas Streicher]

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