Foundation for category theory?

Question

What is the art of knowledge about the foundational issues in category theory ? One possibility is to define categories inside ZFC, but to my understanding there are size issues that do not allow to consider certain usefull objets and constructions of category theory. The other one is an axiomatic definition without any reference to set theory, in the spirit of Lawerie's work in the 70's. Were there progress in this direction since then ? Is there a consensus nowdays about what should be a solid foundation for category theory ?

Answer 1

Category theory can be axiomatised as part of set theory without any difficulty. In order to allow for size issues to play a role one uses Grothendieck universes (so this is basically working within a familiar axiomatic set theory fortified with a suitable universes axiom). One objection to such an approach is that the set theoretic machinery does not fit nicely with the categorical way of doing things. The set-theoretic foundations feel very artificial. Lawvere demonstrated that both set theory and category theory can be axiomatised using category theory.

Is there a consensus of what a foundations for category theory ought to be? Well, first one would need to be clear about what category theory means. Is it $\infty$-category theory? If so, then a lot of work has been done, culminating with the Homotopy Type Theory project and Voevodsky's univalent foundations of mathematics. Still very much work in progress so it is too early to announce it as the foundations of the subject.

There is also the work of Benabou of fibered category theory. In his famous article Benabou argues very convincingly that in naive category theory, a category $C$ is really a functor $\mathsf{Fam}(C)\to \mathbf {Set}$ from the family fibration of $C$ to a category of sets. A foundations for naive category theory then takes the form of the theory of fibrations. There has been quite a lot of work in that direction as well, also in the context of $\infty $-categories.