Dear Eduardo, 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. Regards, Steve Vickers. On Sun, 03 Jul 2011 19:59:16 -0300, "Eduardo J. Dubuc" <edubuc@dm.uba.ar> wrote:
... For example, people which consider the presheaf category Set^((Set_f)^op) (object classifier) often do as if Set_f were canonical and small.
Now, if you work with a Grothendieck base topos “as if it were the category of sets”, you are forced to specify which small category of finite sets you are using, or not ?.
Cheers e.d.
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]