Steven Vickers <S.J.Vickers <at> cs.bham.ac.uk>
2011-07-05 09:37:00 GMT
That's right. Specifically, Set_f here has N for its object of objects,
and something more complicated (but geometrically definable) for its object
of morphisms. That way the correct object classifier is defined for any
base topos. (I'm thinking of Grothendieck toposes here, but I guess it
works for any elementary topos with NNO. I even conjecture it does
something useful for arithmetic universes.)
That's a very strong notion of finiteness constructively. It requires not
only Kuratowski finiteness and decidable equality, but even a decidable
total order. Then the category of such finite sets is essentially small,
equivalent to the Set_f I described above. It is the notion of "finite"
needed in finitely presentable algebras, for example in the theorem that
for a finitary algebraic theory T, the T-algebra classifier is
Set^(T-Alg_fp^op), the topos of Set-values functors from the category of
finitely presented algebras. Again, we want T-Alg_fp to be small.
In my paper "Strongly algebraic = SFP (topically)" I was interested in the
situation where, for a geometric theory T, the classifying topos for T is a
presheaf topos in the form of the topos of Set-valued functors from the
category of finite T-models (and I gave some sufficient conditions for this
to happen). Again, the notion of finite model is this strong notion of
finiteness. However, my main example also involved Kuratowski finite sets,
so the paper discusses in some detail the interplay between the different
notions of finiteness.