The elementary theory of the 2-category of small categories

We give an elementary description of 2-categories Cat (E) of internal categories, functors and natural transformations, where E is a category modelling Lawvere's elementary theory of the category of sets (ETCS). This extends Bourke's characterisation of 2-categories Cat (E) where E has pullbacks to take account for the extra properties in ETCS, and Lawvere's characterisation of the (one dimensional) category of small categories to take account of the two-dimensional structure. Important two-dimensional concepts which we introduce include 2-well-pointedness, full-subobject classifiers, and the categorified axiom of choice. Along the way, we show how generating families (resp. orthogonal factorisation systems) on E give rise to generating families (resp. orthogonal factorisation systems) on Cat (E) ₁, results which we believe are of independent interest.