On the subject of categorical versus set-theoretic foundations there
is too much complicated discussion about structure that misses the
essential point about whether "collections" are necessary.
It doesn't matter exactly what your personal list of mathematical
requirements may be -- rings, the category of them, fibrations,
2-categories or whatever -- developing the appropriate foundational
system for it is just a matter of "programming", once you understand
the general setting.
The crucial issue is whether you are taken in by the Great Set-Theoretic
Swindle that mathematics depends on collections (completed infinities).
(I am sorry that it is necessary to use strong language here in order to
flag the fact that I reject a widely held but mistaken opinion.)
Set theory as a purported foundation for mathematics does not and cannot
turn collections into objects. It just axiomatises some of the intuitions
about how we would like to handle collections, based on the relationship
called "inhabits" (eg "Paul inhabits London", "3 inhabits N"). This
binary relation, written $\epsilon$, is formalised using first order
predicate calculus, usually with just one sort, the universe of sets.
The familiar axioms of (whichever) set theory are formulae in first order
predicate calculus together with $\epsilon$.
(There are better and more modern ways of capturing the intuitions about
collections, based on the whole of the 20th century's experience of algebra
and other subjects, for example using pretoposes and arithmetic universes,
but they would be a technical distraction from the main foundational issue.)
Lawvere's "Elementary Theory of the Category of Sets" axiomatises some
of the intuitions about the category of sets, using the same methodology.
Now there are two sorts (the members of one are called "objects" or "sets"
and of the other "morphisms" or "functions"). The axioms of a category
or of an elementary topos are formulae in first order predicate calculus
together with domain, codomain, identity and composition.
Set theorists claim that this use of category theory for foundations
depends on prior use of set theory, on the grounds that you need to start
with "the collection of objects" and "the collection of morphisms".
Curiously, they think that their own approach is immune to the same
criticism.
I would like to make it clear that I do NOT share this view of Lawvere's.
Prior to 1870 completed infinities were considered to be nonsense.
When you learned arithmetic at primary school, you learned some rules that
said that, when you had certain symbols on the page in front of you,
such as "5+7", you could add certain other symbols, in this case "=12".
If you followed the rules correctly, the teacher gave you a gold star,
but if you broke them you were told off.
Maybe you learned another set of rules about how you could add lines and
circles to a geometrical figure ("Euclidean geometry"). Or another one
involving "integration by parts". And so on. NEVER was there a "completed
infinity".
Whilst the mainstream of pure mathematics allowed itself to be seduced
by completed infinities in set theory, symbolic logic continued and
continues to formulate systems of rules that permit certain additions
to be made to arrays of characters written on a page. There are many
different systems -- the point of my opening paragraph is that you can
design your own system to meet your own mathematical requirements --
but a certain degree of uniformity has been achieved in the way that they
are presented.
We need an inexhaustible supply of VARIABLES for which we may substitute.
There are FUNCTION SYMBOLS that form terms from variables and other terms.
There are BASE TYPES such as 0 and N, and CONSTRUCTORS for forming new
types, such as $\times$, $+$, $/$, $\to$, ....
There are TRUTH VALUES ($\bot$ and $\top$), RELATION SYMBOLS ($=$)
and CONNECTIVES and QUANTIFIERS for forming new predicates.
Each variable has a type, formation of terms and predicates must respect
certain typing rules, and each formation, equality or assertion of a
predicate is made in the CONTEXT of certain type-assignments and
assumptions.
There are RULES for asserting equations, predicates, etc.
We can, for example, formulate ZERMELO TYPE THEORY in this style. It has
type-constructors called powerset and {x:X|p(x)} and a relation-symbol
called $\epsilon$. Obviously I am not going to write out all of the details
here, but it is not difficult to make this agree with what ordinary
mathematicians call "set theory" and is adequate for most of their
requirements
Alternatively, one can formulate the theory of an elementary topos is this
style, or any other categorical structure that you require. Then a "ring"
is a type together with some morphisms for which certain equations are
provable.
If you want to talk about "the category of sets" or "the category of rings"
WITHIN your tpe theory then this can be done by adding types known as
"universes", terms that give names to objects in the internal category
of sets and a dependent type that provides a way of externalising
the internal sets.
So, although the methodology is the one that is practised by type theorists,
it can equally well be used for category theory and the traditional purposes
of pure mathematics. (In fact, it is better to formalise a type theory
such as my "Zermelo type theory" and then use a uniform construction to
turn it into a category such as a topos. This is easier because the
associativity of composition is awkward to handle in a recursive setting.
However, this is a technical footnote.)
A lot of these ideas are covered in my book "Practical Foundations of
Mathematics" (CUP 1999), http://www.PaulTaylor.EU/Practical-Foundations
Since writing the book I have written things in a more type-theoretic
than categorical style, but they are equivalent. My programme called
"Abstract Stone Duality", http://www.PaulTaylor.EU/ASD is an example of the
methodology above, but far more radical than the context of this question
in its rejection of set theory, ie I see toposes as being just as bad.
My personal opinion is that one should consider the 2-category of categories, rather than the 1-category of categories. I think the axioms one wants for such an "ET2CC" will be something like:
- Firstly, some exactness axioms amounting to its being a "2-pretopos" in the sense I described here: http://ncatlab.org/michaelshulman/show/2-categorical+logic . This gives you an "internal logic" like that of an ordinary (pre)topos.
- Secondly, the existence of certain exponentials (this is optional).
- Thirdly, the existence of a "classifying discrete opfibration" $el\to set$ in the sense introduced by Mark Weber ("Yoneda structures from 2-toposes") which serves as "the category of sets," and internally satisfies some suitable axioms.
- Finally, a "well-pointedness" axiom saying that the terminal object is a generator, as is the case one level down with in ETCS. This is what says you have a 2-category of categories, rather than (for instance) a 2-category of stacks.
Once you have all this, you can use finite 2-categorical limits and the "internal logic" to construct all the usual concrete categories out of the object "set". For instance, "set" has finite products internally, which means that the morphisms $set \to 1$ and $set \to set \times set$ have right adjoints in our 2-category Cat (i.e. "set" is a "cartesian object" in Cat). The composite $set \to set\times set \to set$ of the diagonal with the "binary products" morphism is the "functor" which, intuitively, takes a set $A$ to the set $A\times A$. Now the 2-categorical limit called an "inserter" applied to this composite and the identity of "set" can be considered "the category of sets $A$ equipped with a function $A\times A\to A$," i.e. the category of magmas.
Now we have a forgetful functor $magma \to set$, and also a functor $magma \to set$ which takes a magma to the triple product $A\times A \times A$, and there are two 2-cells relating these constructed from two different composites of the inserter 2-cell defining the category of magmas. The "equifier" (another 2-categorical limit) of these 2-cells it makes sense to call "the category of semigroups" (sets with an associative binary operation). Proceeding in this way we can construct the categories of monoids, groups, abelian groups, and eventually rings.
A more direct way to describe the category of rings with a universal property is as follows. Since $set$ is a cartesian object, each hom-category $Cat(X,set)$ has finite products, so we can define the category $ring(Cat(X,set))$ of rings internal to it. Then the category $ring$ is equipped with a forgetful functor $ring \to set$ which has the structure of a ring in $Cat(ring,set)$, and which is universal in the sense that we have a natural equivalence $ring(Cat(X,set)) \simeq Cat(X,ring)$. The above construction then just shows that such a representing object exists whenever Cat has suitable finitary structure.
One can hope for a similar elementary theory of the 3-category of 2-categories, and so on up the ladder, but it's not as clear to me yet what the appropriate exactness properties will be.
Best Answer
I don't agree that this is what (most) categorists who are interested in foundations are doing.
It is true that Lawvere in the mid-60's (and perhaps to this day) wanted to develop a theory of categories independent of a theory of sets, but I don't think that represents the main thrust of modern-day categorical work on "foundations". Much more work has been directed toward developing a full-fledged categorical theory of sets, either as in Lawvere's Elementary Theory of a Category of Sets and extensions thereof, or understanding classical theories of sets such as ZF through a categorical lens, as in Algebraic Set Theory. There is also ongoing discussion of what strength of set theory is suitable for doing what category theorists would like to do. As one can see with even a casual perusal of such work, there is no antagonism toward set theory per se, or a desire to somehow get away from sets.
I think some confusion might stem from over-hasty identification of set theory with a "canonized" form of set theory, such as ZFC (or something in that family such as Gödel-Bernays set theory), based on a single binary predicate called "membership". In ordinary ZFC, a set is characterized by its membership tree, so that the elements of sets are sets themselves, possessing their own internal structure. This may be termed a "materialist" form of set theory (material because elements of sets are considered as having "substance"). If there is antagonism toward this type of set theory on the part of some category theorists, it's because it lends itself to a conception of "set" that is largely irrelevant to the actual practice of core mathematics, insofar as mathematicians don't care what elements are "made of".
The prevailing trends of mathematical practice today and throughout most of the twentieth century promote a more "structuralist" view: that what counts is not what the elements of a structure "are" particularly, but rather how they are interrelated in a structure, and where two structures are considered abstractly the same if they are isomorphic. This seems like a truism today, but it is precisely this view which drives a more categorically-minded view, which looks toward not what sets "are", but of how we use them, what abstract constructions we want to perform on them, and so on. Thus, concepts such as "power set" are in this view more relevantly captured by suitable universal properties which serve to characterize their structure up to specified isomorphism. A theory of sets which takes this point of view seriously and axiomatically may be termed a "structural set theory".
Thus the real contrast is between "material" and "structural" theories of sets, with category theorists tending to prefer structural set theory. An example of such is Lawvere's aforementioned Elementary Theory of the Category of Sets (ETCS). A different and more recent example is Mike Shulman's SEAR (Sets, Elements, and Relations), which you can read about at the nLab.
As for practical benefits of structuralist set theory: they are huge! It should be borne in mind that elementary topos theory was largely inspired by Lawvere's insight that Grothendieck toposes themselves model most of the axioms of the kind of structuralist set theory he was investigating in ETCS, and this has been revolutionary. This answer is already long enough, so I won't enter on a discussion of that here.