# Is there a formal class theory that suffices to formalize the basic notions of category theory?

Is there a formal class theory that suffices to formalize the basic notions of category theory? I think the usual formalizations of class theory like Neumann-Bernays-Gödel or Morse-Kelley don't suffice (for the latter, see the thread Morse-Kelley and category theory) to formalize the basic notions of category theory. For example, a category is a tuple consisting of a (possibly proper) class of objects and a (possibly proper) class of morphisms and a composition operation. Also one wants to consider class-functions to formalize the notion of a functor.

• How about ZFC plus an assumption that there are arbitrarily large inaccessible cardinals? From what I hear this appears to be a common setting for category theory these days; it implies that everything you could reasonably be interested in will take place inside some Grothendieck universe. – Henning Makholm Oct 9 '16 at 13:06
• @HenningMakholm: Yes, this is a good solution. But I am somehow interested in how one can formalize the "proper class vs. set" approach to category theory. – user376483 Oct 9 '16 at 13:07
• More important is how to formalize ideas such as categories of categories. I think they are called $1$-categories ? – Rene Schipperus Oct 9 '16 at 13:25
• @ReneSchipperus: Yes, that's also interesting: Is there a formal theory which formalizes the notion of "collection of classes"? – user376483 Oct 9 '16 at 13:26
• Yeah, and what about "conglomerates of collections of classes" ? – Rene Schipperus Oct 9 '16 at 13:28