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)_1, results which we believe are of independent interest.
Keywords: Set theory, elementary toposes, internal categories, 2-categories, elementary theories
2020 MSC: 03B30, 03E30, 03G30, 18A15, 18B05, 18B25, 18B50, 18D40, 18N10
Theory and Applications of Categories, Vol. 43, 2025, No. 8, pp 196-242.
Published 2025-03-23.
TAC Home