Morse-Kelley and category theory

Question

How much of category theory can be formalized within Morse-Kelley? Is it even possible to define the notion of a category as a tuple consisting of a class of objects, a class of morphisms, and a comoposition operation for morphisms such that the usual axioms of category theory hold? Then, is it possible to talk about the category of sets or groups for example as an own object?

Answer 1

You can't define a category as a tuple per se, but you can define it as a list of three classes (not formally put into a tuple). There is a formula $\text{Cat}(A,B,C)$ in the language of set theory so that classes $(A,B,C)$ satisfy $\text{Cat}(A,B,C)$ if and only if $A$ is a class of structures, $B$ is a class of morphisms between structures in $A$, $C$ is a class function telling how to compose the morphisms from $B$, and all together $A$, $B$, and $C$ satisfy the axioms of a category.

Because the quantifiers in MK are over classes, this makes it possible to quantify over categories. To write "There is a category such that ..." we would write $$ (\exists A)(\exists B)(\exists C)[\text{Cat}(A,B,C) \land \ldots]. $$

Similarly, because MK has comprehension axioms that produce classes, we can use the comprehension axioms to form the category of all groups, the category of all sets, etc.

We can also quantify over functors. A functor would consist of two classes $E,F$ so that $E$ is a class of mappings between objects and $F$ is a class of mappings between morphisms, so that $E$ and $F$ together satisfy the axioms of a functor. So the formalization of "Let $X$ and $Y$ be categories and let $F$ be a functor from $X$ to $Y$" would begin with eight existential quantifiers.

We can also represent a tuple of classes indirectly, e.g we could represent a tuple of classes $(C_0,C_1,C_2)$ as the class of all pairs $(0,x)$ with $x\in C_0$ or $(1,y)$ with $y\in C_1$ or $(2,z)$ with $z \in C_2$. This is just syntactic sugar; it allows us to replace three quantifiers with one, but formally three quantifiers works just as well.