categories: Re: Characterizing FinSet up to equivalence

[S Vickers <s.j.vickers@open.ac.uk>]

Vaughan Pratt writes:
>Now some logicians such as Sol Feferman, and one imagines at least a
>few category theorists, view category theory as built on set theory.
>...  Where one sits in this spectrum is
>presumably correlated with how strongly one feels that set theory has been
>smuggled into the following.
>
>...
>
>Claim.  Let C be a category with finite sums and final object 1.  If 1 is
>a strongly indecomposable generator and every object is either initial or
>a successor, ...
>
>(Set, FinSet, and Stone all meet these conditions on C, ...

Set theory has been smuggled into the whole argument in an all-pervading
way, and moreover in a specifically classical form. This causes problems
when you start exploring more adventurously the nature of sethood. The
argument about finiteness is then much less help than it might have
appeared at first. 

As a particular example that category theory helps us to explore, we know
there are benefits to be had from thinking of sheaves as sets (continuously
parametrized by points of spaces, but the trick is to keep the parameter
under wraps). They are benefits that do not depend on having recourse to
some fixed classical notion of "actual" sets, unparametrized.

There are important notions of finiteness for sheaves that require
investigation. For instance, "Kuratowski finiteness" underlies the
logically important notion of finitely bounded universal quantification.
But the categories of sheaves do not in general get off the ground with
Vaughan's results, since we do not have that every sheaf is either initial
or a successor. Hence the results make little contribution to understanding
finiteness for sheaves.

Let me present another concrete set theory that, to my mind, provides
foundations just as good as those of classical set theory.

Buy a lorry load of ready-mixed concrete. Spread it evenly over your front
drive. Wade into the middle of it and wait for it to set.

Now if you want to explore beyond the margins of your front drive you will
be safe, because you have a good solid bit of concrete to support you.

Harsh? To bring the sheaves into classical set theory requires quite
cumbersome machinery. We do better to find out what really makes the
sheaves work rather than insistently reducing them to a notion of set that
we know to be ill-matched. Only then can we, as the psalm puts it, "return
with songs of joy, carrying sheaves with us".

Steve Vickers.