Steve Awodey has a quite short but fascinating paper now available online called ‘From Sets to Types to Categories to Sets’, inter alia saying something tolerably accessible about the significance of his recent technical work. Here’s the first paragraph:
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.
And here’s the last paragraph. Awodey has been noting the set theory gives constructions features that are not mathematically salient — ‘no topologist or algebraist is concerned with the logical type or ordinal rank of a manifold or module’ — though ‘they can serve a useful purpose in foundational work by providing the concrete data for specifications and calculations, facilitating constructions and proofs.’
By contrast, the purely structural approach of category theory sometimes offers comparatively little such “extra” structure to hold on to. Practically speaking, it can be harder to give an invariant proof. That is why it’s good to know that such logical structure can always be introduced into a category when needed; the devices of introducing an internal logic or a set theoretic structure into a category, as sketched in the foregoing sections, were originally developed in order to benefit from their advantages, much like introducing local coordinates on a manifold for the sake of calculation. The analogy is quite a good one: no one today regards a manifold as involving specific coordinate charts, and one generally works with coordinate free methods so that the results obtained will apply directly|this is the modern, structural approach. But at times it can still be useful to introduce coordinates for some purpose, and this is unobjectionable, as long as the results are invariant. So it is with categorical versus logical foundations: category theory implements the structural approach directly. It admits interpretations of the conventional logical systems, without being tied to them. Category theory presents the invariant content of logical foundations.
Anyone interested in foundational issues will want to read the paragraphs in between the first and last! (Thanks to Richard Zach, over at LogBlog, for the link.)