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 ?
-
2$\begingroup$ Axiomatic systems such as Lawvere's ETCC are not used in practice. Some people do study things like "2-categories of enriched categories", however. Perhaps the Riehl–Verity work on the 2-category of quasicategories will change that. $\endgroup$– Zhen LinMay 12, 2021 at 9:58
-
$\begingroup$ Why are axiomatic systems not used in pratice ? Could you please give me some references for the Riehl-Verity work ? $\endgroup$– huurdMay 12, 2021 at 10:00
-
1$\begingroup$ Unfamiliarity is one reason, inadequacy is another. It seems Riehl and Verity have collected their work into a textbook now. $\endgroup$– Zhen LinMay 12, 2021 at 10:05
-
$\begingroup$ Oh wonderfull thanks for the textbook ! Which kind of inadequacy do you refer to ? $\endgroup$– huurdMay 12, 2021 at 11:33
-
2$\begingroup$ Isn't Riehl-Verity about something completely different ? Namely, not about set-theoretic foundations for category theory, but about (2-)category theoretic foundations for $(\infty,1)$-categories ? For set theoretic issues, I always recommend Shulman's paper "Set theory for category theory" $\endgroup$– Maxime RamziMay 13, 2021 at 13:54
1 Answer
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.
-
$\begingroup$ Which article of Benabou are you refering at ? $\endgroup$– huurdMay 14, 2021 at 6:04
-
1$\begingroup$ Fibered categories and the foundations of naive category theory. $\endgroup$ May 14, 2021 at 10:14