The Elementary Theory of the $2$-Category of Small Categories
Date:
Lawvere’s Elementary Theory of the Category of Sets (ETCS) posits that the category Set is a well-pointed elementary topos with natural numbers object satisfying the axiom of choice. This provides a category theoretic foundation for mathematics which axiomatises the properties of function composition in contrast to Zermelo-Fraenkel set theory with the axiom of choice (ZFC), which axiomatises sets and their membership relation. Furthermore, ETCS augmented with the axiom schema of replacement can be shown to be equiconsistent with ZFC.
In this talk, I will present a categorification of ETCS which axiomatises the 2-category of small categories, functors and natural transformations; this is the elementary theory of the 2-category of small categories (ET2CSC) of the title. This extends Bourke’s characterisation of categories internal to a category E with pullbacks to the setting where E satisfies the extra properties of ETCS. Important 2-categorical definitions I will introduce are 2-well-pointedness, the full subobject classifier and the categorified axiom of choice. The main conclusion is that ET2CSC is `Morita biequivalent’ with ETCS, meaning that the two theories have biequivalent 2-categories of models.
I will also describe how Shulman and Weber’s ideas on discrete opfibration classifiers can be used to incorporate replacement, in a way reminiscent of algebraic set theory.
This talk is based on joint work with Adrian Miranda.