The elementary theory of the 2-category of small categories

We give an elementary description of $2$-categories $\mathbf{Cat}(\mathcal{E})$ of internal categories, functors and natural transformations, where $\mathcal{E}$ is a category modelling Lawveres elementary theory of the category of sets (ETCS). This extends Bourkes characterisation of $2$-categories $\mathbf{Cat}(\mathcal{E})$ where $\mathcal{E}$ has pullbacks to take account for the extra properties in ETCS, and Lawveres 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 $\mathcal{E}$ give rise to generating families (resp. orthogonal factorisation systems) on $\mathbf{Cat}(\mathcal{E})$, results which we believe are of independent interest.