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

101 Views Asked by At

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.