Cat (Category)

Cat is the 2-Category of categories:

• Objects are categories
• Arrows are functors
• 2-arrows are natural transformations Note that to prevent contradiction, there is an infinite hierarchy of such categories in which no type contains itself (see Universe Polymorphism). So $Ca{t}_{\ell +1}=Category({\mathbf{Cat}}_{\ell })$ is the category of ${\mathbf{Cat}}_{\ell }$ categories, $\forall \ell \in \mathbb{N}$ .

There is not a category of categories since we don’t always have equality on functors. There is a category of strict categories.