Class-sized category theory in ZFC: definable-class schemas, small and locally small categories, and why $\mathbf{CAT}$ is not formed

The word class in this development is an abbreviation for a formula in the language of set theory, as described by The first-order language of set theory: $\in$, $=$, formulas with parameters, and class abbreviations. It is not an additional set. A category may therefore have a definable class of objects and a definable class of morphisms. Quantification over such a category is a schema: each use expands to an ordinary formula of ZFC.

A category is small when its objects and morphisms form sets, and locally small when each hom-collection is a set. The category $\mathbf{Cat}$ used below has small categories as objects; its hom-categories are sets or locally small categories as asserted in the relevant result. We do not form a category $\mathbf{CAT}$ of all large categories. Doing so as though all classes were members of a larger set would conflict with the same size obstruction exhibited for the ordinals by Burali-Forti: there is no set of all ordinals. Class recursion, when used, is only the definable schema licensed by Transfinite recursion.