Definition 4.9.14.  Let u ∈ ℕ. We define:
Cat(u) := [Catu(Fun(A, B))A,B ∈ Catu(idC)C ∈ Catu(∘)D,E,F ∈ Catu]u+1 is a/an (u + 1)-small category
Remarks.

This defines the category of small categories, or, more generally, a category in $../../Essentials/Numbers/Natural/sum(m = u, n = $../../Essentials/Numbers/Natural/number(value = 1)) of all categories in u.

References.