Categories for the Working Philosopher: 1–3
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’. 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?
The post Categories for the Working Philosopher: 1–3 appeared first on Logic Matters.
