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.