There are a number of foundational schemes out there. ZFC set theory is perhaps the most widely known, but of course you can also develop math in type theory. And you can also do it in category theory. So what’s the difference? Steve Awodey has an answer in a preprint of a paper, now posted on his web site: “From Sets to Types to Categories to Sets“. Here’s the introductory paragraphs:
Three different styles of foundations of mathematics are now commonplace: set theory, type theory, and category theory. How do they relate, and how do they differ? What advantages and disadvantages does each one have over the others? We pursue these questions by considering interpretations of each system into the others and examining the preservation and loss of mathematical content thereby.
In order to stay focused on the “big picture”, we merely sketch the overall form of each construction, referring to the literature for details. Each of the three steps considered below is based on more recent logical research than the preceding one. The first step from sets to types is essentially the familiar idea of set theoretic semantics for a syntactic system, i.e. giving a model; we take a brief glance at this step from the current point of view, mainly just to fix ideas and notation. The second step from types to categories is known to categorical logicians as the construction of a “syntactic category”; we give some specifics for the benefit of the reader who is not familiar with it. The third step from categories to sets is based on quite recent work, but captures in a precise way an intuition from the early days of foundational studies.
With these pieces in place, we can then draw some conclusions regarding the differences between the three schemes, and their relative merits. In particular, it is possible to state more precisely why the methods of category theory are more appropriate to philosophical structuralism.
UPDATE: Peter Smith had the good judgment of also quoting from the conclusion, where Steve makes the point that the advantage of the category-theoretic approach is that, of the three approaches, category theory is the system that allows formalization of only the structurally invariant mathematical facts, those that don’t depend on specific features of the foundational scheme (say, where in the cumulative hierarchy something lives)–although you can have all that extra structure in the category-theoretic setting, if you want or need it.