The elementary theory of the 2-category of small categories (Q7006825)

\textit{F. W. Lawvere}'s elementary theory of the category of sets (ETCS) [Proc. Natl. Acad. Sci. USA 52, 1506--1511 (1964; Zbl 0141.00603); Repr. Theory Appl. Categ. 2005, No. 11, 1--35 (2005; Zbl 1072.18005)] provides an important fragment of a category-theoretic foundation of mathematics, but is strictly weaker than the traditional foundation of mathematics incarnated by Zermelo Fraenkel set theory with the axiom of choice (ZFC). Precisely speaking, ZFC is equiconsistent with ETCS with the axiom schema of replacement [\textit{G. Osius}, J. Pure Appl. Algebra 4, 79--119 (1974; Zbl 0282.02027)].\N\NThis paper proposes a different categorification of ETCS capturing the natural two-dimensional structure of the 2-category of small categories, which is called the elementary theory of the 2-category of small categories (ET2CSC). The main result is that ET2CSC is Morita biequivalent to ETCS, meaning that the two theories have biequivalent 2-categories of models.