In his PhD thesis and subsequent papers, Lawvere gave a finite axiomatization of the properties of function composition. Known as the elementary theory of the category of sets (ETCS), this framework can be used to describe many set theoretical constructions used in everyday mathematical practice. The main gap between ETCS and traditional foundations such as ZFC is the axiom of replacement, which allows more sophisticated constructions such as transfinite recursion.
Lawvere also called for a similar axiomatization of the two-dimensional structure of categories, functors, and natural transformations. In this talk I will describe a characterisation of 2-categories Cat(E) of categories internal to a model of ETCS. This builds upon Bourke’s characterisation of Cat(E) when E just has pullbacks. The resulting theory is the elementary theory of the 2-category of small categories (ET2CSC) of the title. The main result is that the 2-categories of models of ETCS and ET2CSC are biequivalent.
Time permitting (or in a follow up talk!), I will also describe how the two-dimensional setting supports a convenient way of incorporating the axiom of replacement, albeit in a non-elementary way. This uses Weber’s discrete opfibration classifiers and is inspired by the categories of small maps from algebraic set theory.
This talk is based on joint work with Calum Hughes.