The Elementary Theory of the 2-Category of Small Categories
Adrian Miranda – 21 February 2024
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.
Back