Categories for the Working Philosopher, edited by Elaine Landry (OUP), was first published in 2017, and I briefly noted this collection when it came out as seeming to be a very mixed bag. Since my mind is back on matters categorial, and the book has been recently paperbacked, I thought I’d take another look.
Landry describes the first eleven essays as concerning the “use of category theory for mathematical, foundational, and logical purposes”. The remaining seven pieces are on scattered applications of category theory (though there seems to be nothing on why it has come to be of such central concern to theoretical computer science). I’ll probably only comment here on the earlier essays, and I’ll take them in the published order, starting with the first three.
‘The roles of set theories in mathematics’ by Colin McLarty takes up what is by now a familiar theme — that ZFC radically overshoots as an account of what ‘ordinary mathematics’ requires by way of background assumptions about sets. McLarty in particular takes a look at the set-theoretic preliminaries expounded in two classic texts, by Munkres on topology and Lang on algebra, and comments on their relatively modest character. Now, neither Munkres or Lang gives a regimented summary of his set-theoretic assumptions in axiomatic form: but if we did so, what would it look like? Arguably like ETCS, the theory so neatly presented in Tom Leinster’s well-known ‘Rethinking set theory’ whose aim is, as he puts it, to show that “simply by writing down a few mundane, uncontroversial statements about sets and functions, we arrive at an axiomatization that reflects how sets are used in everyday mathematics.”
Now, ‘ETCS’ is of course short for the ‘Elementary Theory of the Category of Sets’ developed by Lawvere and its original idiom was categorial. But Leinster is at pains to point out that the axioms of this set theory, in his presentation, do not involve any essentially categorial notions — they just talk about sets and functions (without reducing the functions to sets, by the way). McLarty explores a little further in a helpful and interesting way, e.g. telling us more about how variant stronger set theories can be seen as expansions of ETCS.
But I can imagine some thinking that the interest here is primarily set-theoretic rather than in the (apparently dispensable?) categorial idiom. I doubt that McLarty sees it like that! — but then those readers would have probably liked to hear more from him here about quite how he does see ETCS to be more intertwined with category theory.
The next paper is, by my lights, pretentious arm-waving by David Corfield on ‘Reviving the philosophy of geometry’: you can give this a miss.
Next up, Michael Shulman writing about ‘Homotopy type theory: a synthetic approach to higher equalities’: you can download the paper here. Now, Shulman has elsewhere shown a considerable gift for what you might call the higher exposition — explaining, unifying, organising difficult material. His much-referenced paper ‘Set theory for category theory‘ is indispensable. But this present paper is pretty hard going — surely rather too compressed and allusive (would someone who had never before encountered Einstein’s hole argument get what is going on? more to the point, is the supposedly crucial distinction between the rules of a type theory and axioms of a set theory made transparently clear?). I’ll certainly not try to summarize, then. But despite its density, the piece is helpful enough to be worth struggling with, if you want to get some glimmer of what the programme of homotopy type theory/univalent foundations is.
However, as Shulman tells us at the outset, HoTT is a “surprising synthesis of constructive intensional type theory and abstract homotopy theory” and neither of those is essentially categorial from the off. Indeed, in the foundational text, Homotopy Type Theory: Univalent Foundations of Mathematics, category theory doesn’t get mentioned until p. 377! So we might wonder: interesting though HoTT’s programme is as “a new foundation for mathematics and logic” (in Landry’s words), in what sense exactly is this programme essentially categorial in nature?
there seems to be nothing on why it has come to be of such central concern to theoretical computer science — My view is that explaining why that happened is a job for sociology, psychology, and history, so it’s not surprising that this book doesn’t do it. It could, of course, describe some of the uses some computer scientists have found for category theory; that would not, however, explain *why* it’s become of central concern. (I see it as similar to explaining why logical programming came to seem important in AI back in the 1980s.)
(I’m tempted to say it’s not actually category theory that’s become prominent — it’s type theory, with category theory getting in via type theory — but that’s not quite right either.)
In any case, part of the explanation is that theoretical computer scientists need something to be theoretical about, and the ‘low-hanging fruit’ in computability and complexity had already been picked. Another part is that object-oriented programming ceased to be cool.
My other comments are about the two older papers mentioned.
I don’t think I’ve read Mike Shulman’s ‘Set theory for category theory’ before. I think it’s very good and refreshingly free of attempts to make set theory seem fundamentally misguided.
And in From Set Theory to Type Theory (January 7, 2013), Shulman makes a point that will be useful below.
Leinster’s ‘Rethinking set theory, on the other hand, which I have read before, strikes me as quite tendentious. I don’t understand how anyone can read it without objecting to anything at all. Consider this, for example:
How can anyone read that and not think something like, “Wait a minute! No one who’s looked at category theory thinks the motive is to replace all talk of sets with talk of categories, or anything like that. They know category theorists still want to talk about sets. There’s even a category, Set.”
Some of the more ideological category theorists do, however, want to replace the ‘orthodox’ set-theoretic foundations of mathematics with a category-theoretic alternative; they think something like ETCS should displace ZFC in its foundational role and as the set theory that would normally be used; and, more generally, they reject the material conception of sets and prefer a structural one.
Leinster’s “it is set theory” does not refute suspicions on those lines about the underlying motive. It can even seem to confirm them, for why else would he say ETCS “is set theory” rather than “is a set theory”?
There’s a useful discussion of the ‘Rethinking Set Theory’ paper at The n-Category Café, initiated by Tom Leinster.
Note that Leinster begins by saying “Over the last few years, I’ve been very slowly working up a short expository paper — requiring no knowledge of categories — on set theory done categorically.” (Emphasis added)
Which is why, even though ETCS can be presented, initially, without mentioning “any essentially categorial notions”, the paper soon shows how elements (which don’t fit a categorical approach) can be replaced by functions. (That move already means that this approach does demand more mathematical sophistication than ordinary set theory.)
This from ‘Rethinking set theory’ p 2 nonetheless seems reasonable:
However, bearing in mind Shulman’s observation that although “the basic objects of ZFC and ETCS are both called ‘sets’, … they behave so differently that it can be confusing to use the same name for both”, comments such as this one from François G. Dorais become interesting:
Naturally, that’s rejected. It would mean accepting that sets have the sort of membership structure they have in ZFC, that ETCS would not displace ZFC, and that what even Shulman sometimes calls ‘ZF hegemony’ would continue.
Having spent a lot of time talking to the HoTT people and grappling with their intuitions, I’d argue that their answer to your last question is that algebraic topology (or, really, homotopy theory as its own branch of mathematics) *is* inherently category theoretic. The nlab has a page on ‘computational trinitarianism’ and over time it’s evolved to the point where the category theoretic perspective has been subsumed by the homotopic perspective. They would argue that HoTT is essentially categorial in nature because homotopy theory is itself ‘the study of ∞-categories’.
Yes, I’m sure that’s the story! When I wrote “we might wonder …” I was thinking of the intended(?) readership of this collection which Elaine Landry aims to be “accessible to a general audience”, who might need the dots to be joined up!