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.

  • 1
    $\begingroup$ 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. $\endgroup$ – Henning Makholm Oct 9 '16 at 13:06
  • $\begingroup$ @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. $\endgroup$ – user376483 Oct 9 '16 at 13:07
  • $\begingroup$ More important is how to formalize ideas such as categories of categories. I think they are called $1$-categories ? $\endgroup$ – Rene Schipperus Oct 9 '16 at 13:25
  • $\begingroup$ @ReneSchipperus: Yes, that's also interesting: Is there a formal theory which formalizes the notion of "collection of classes"? $\endgroup$ – user376483 Oct 9 '16 at 13:26
  • $\begingroup$ Yeah, and what about "conglomerates of collections of classes" ? $\endgroup$ – Rene Schipperus Oct 9 '16 at 13:28

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.