FOM: HA/PA, categorical (pseudo) foundations

[Vaughan Pratt]

Egalitarian nitpicking follows.  -vp


From: Harvey Friedman
>By far the most interesting thing about
>category theory is the universal mapping properties.

I would agree with this if you would agree that "By far the most
interesting thing about set theory is functions."

Functions and universality are important and early steps in the
development of respectively set theory and category theory.  A little
green critter trained to think categorically and introduced later on
to sets might well find functions the most profound thing about sets,
as being the first aspect of sets about which he is able to formulate
questions that his world-view makes interesting to him.

>Can we define what a
>universal mapping property is in general, and determine all of the
>universal mapping properties (at least under a very general definition of
>universal mapping properties)? If so, then one could hope to reaxiomatize
>set theory as the set theory that supports all of the universal mapping
>properties.

Why not ask the category theorists themselves?  They would be in the
best position to answer this, having had decades to ponder exactly these
sorts of questions.  If you intended the question to be more than merely
rhetorical, mail it to categories at mta.ca and see what response you get.

From: Colin McLarty
>One known non-foundational characterization may help. We assume the
>category "set" of sets is given, but then use universal mapping properties
>(given as adjoints) to describe all and only the categories equivalent to it:
>>An adjoint characterization of the category of sets 
>>  Robert Rosebrugh and R. J. Wood 
>> Proceedings of the American Mathematical Society 122(1994), 409-413
>>Abstract :
>>If a category B with Yoneda embedding Y : B ---> CAT(B^op,set) has an adjoint >>string, U -| V -| W -| X -| Y, then B is equivalent to set.

To what extent does this (extremely nice) universal property of Set
(synonyms: "set", "sets") really characterize Set?  The difficulty is that
"Set" appears in the antecedent.

Had the theorem read

>>If a closed category B with Yoneda embedding Y : B ---> CAT(B^op,B) has
>>an adjoint string, U -| V -| W -| X -| Y, then B is equivalent to Set.

then this would be a *somewhat* better characterization.  (Note that the
singleton category B=1 with the evident closed structure satisfies the
condition.  Ruling out this case would be like including Consis(T) as an
axiom of T.)

I say "somewhat" because CAT, the (superlarge) category of all large
categories and their functors, is assumed by Rosebrugh and Wood themselves
to be defined in terms of SET, the category of all large sets.  So even
with Set replaced by B we still haven't cleanly removed our preconceptions
about sets from the premises.  McClarty would then need to step in and use
his axiomatic approach to remove this dependence of CAT on SET assumed
by Rosebrugh and Wood, who would then need to turn around and judge to
what extent Colin had succeeded in doing so.

If you have to assume Set is given in order to even state the theorem,
how can you tell how much the theorem has to say about Set?

At a bare minimum you should be able to produce some category C for
which the following is false:

>>If a category B with Yoneda embedding Y : B ---> CAT(B^op,C) has an adjoint
>>string, U -| V -| W -| X -| Y, then B is equivalent to C.

Otherwise the theorem cannot be read as saying anything at all about Set.

If my C-parametrized version of the theorem were false for all C except
Set, that would be a lot more interesting (but we still have CAT in
the antecedent).

Can you characterize the extent to which this theorem characterizes Set?
Does it even do so at all?  If you have to work very hard to find a
single C refuting my parametrized variant, I would say the original
(unparametrized) theorem gives no understandable characterization of Set
at all, and that's even before we take the concern about the set-theoretic
basis for CAT into account.

Vaughan Pratt