FOM: HA/PA, categorical (pseudo) foundations

[Colin McLarty]

Friedman writes:

>I have a positive proposal for making something out of category
>theory/topos theory for f.o.m. By far the most interesting thing about
>category theory is the universal mapping properties. 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.

        Do you mean to change the standard definition of universal mapping
properties in some way? My following remarks use it.

        You cannot defining set theory as supporting "all" universal mapping
properties, since there are universal mapping properties that can only occur
in a trivial category (equivalent to a category with only one object and one
arrow). But you can define set theory as supporting certain universal
mapping properties, and then there is great scope for choosing which ones
and what kind of unified description you could give for the ones you choose.

        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.


        More foundationally, three salient universal mapping properties of
sets are: There exist cartesian products of sets and projection functions,
there exist function sets B^A and evaluation functions ev:(B^A)xA-->B, each
subset has a characteristic function. These are the topos axioms.  

Colin