# Is category theory constructive?

Roughly: This question concerns the process and the constructive nature of formalizing and proving category theoretic statements within $\textsf{ZFC}$.

$\textsf{ZFC}$ can only talk about sets, while proper classes live in the metatheory as explicit first order formulae. Statements about classes are always to be interpreted as schemes in the metatheory of $\textsf{ZFC}$ beginning with some (meta-theoretic) quantification "For any formula $\phi(x)$, ...".

In particular, this applies to non-small categories. A statement about some family of categories has to be interpreted as a scheme in the metatheory beginning with "For any three formulas $\text{Obj}(x)$, $\text{Mor}(x,y,z)$, $\text{Comp}(x,y,z,f,g,h)$ defining the objects, morphisms and compositions of a category [maybe some extra properties], ...". The meta-theoretic quantification gets richer in case several categories and/or functors between categories and/or transformations between functors are given.

The above concerns the translation of the assumptions of a category-theoretic statement into the meta-theory of $\textsf{ZFC}$. As for the conclusion, it might be that it just concerns some properties of the categories under consideration, like 'In any abelian category epimorphisms are stable under pullback'; in this case, the conclusion is just a single formula of $\textsf{ZFC}$, so the whole statement translates into a meta-theoretic scheme of the form "For any formulas $\phi,\psi,...$, $\textsf{ZFC}\vdash \text{(Some explicit formula involving }\phi,\psi,...\text{)}$".

This is different if the conclusion concerns the existence of certain categories, functors, natural transformations... Again, as one cannot quantify over proper classes within $\textsf{ZFC}$, the formalization of such a statement as a scheme in the metatheory of $\textsf{ZFC}$ requires that the objects whose existence is claimed can be explicitly defined, within the finitistic meta-theory, as certain first-order formulae.

Observation: Proofs of statements about the existence of categories and functors have to be explicit/constructive when they ought to be formalizable within $\textsf{ZFC}$

My question now simply is:

Question A: Are most existence results of standard category theory indeed constructive?

I have doubts that this is the case, which would mean that $\textsf{ZFC}$ is really insufficient for formalizing category theory, even in principle. For example, consider the statement:

Example: Any fully faithful and essentially surjective functor is an equivalence

How to formalize this in $\textsf{ZFC}$? Is there any way to derive from any family of formulas defining two categories ${\mathscr C},{\mathscr D}$ and a fully faithful and essentially surjective functor ${\textbf F}:{\mathscr C}\to{\mathscr D}$ between them three formulas defining an inverse functor ${\textbf G}: {\mathscr D}\to {\mathscr C}$ and equivalences ${\textbf F}{\textbf G}\cong\text{id}_{\mathscr D}$ and ${\textbf G}{\textbf F}\cong\text{id}_{\mathscr C}$?

As in the development of (small) category theory within $\textsf{ZF}$, one might try to resolve this by using anafunctors instead of functors. That is, statements about functors should be formalized as schemes in the meta-theory concerning formulas defining anafunctors; this essentially means that we ignore this single issue of explicitly inverting fully faithful and dense functors by formally adding their inverses.

Question B: Does Question A have a positive answer in case functors are always formalized as anafunctors?

For example, one might now consider more complicated statements like the adjoint functor theorem and ask whether they can be formalized within $\mathsf{ZFC}$ when anafunctors are used instead of functors. In other words: are their proofs constructive up to inverting fully faithful and dense functors?

Clarification: (1st edit) By "constructive" I do only refer to the proofs of existence statements about categories and functors: I wonder whether (maybe up to the formal inversion of fully faithful and dense functors through the use of anafunctors) from proofs of such statements one can extract explicit first-order formulae defining the desired categories and (ana)functors.

Then, and only then, the statement could indeed by formalized as a scheme in the meta-theory of $\textsf{ZFC}$.

I do not necessarily want to replace $\textsf{ZFC}$ by $\textsf{ZF}$ or even some intuitionistic set theories. My primary goal is to understand whether $\textsf{ZFC}$ can in principle serve as a home for basic category theory through the use of schemes in the meta-theory.

For example, although unlikely, it is not clear to me whether there could be an algorithm turning formulae describing a fully faithful and dense functor into another formula describing a quasi-inverse.

• I recently found this nice expository paper: [Shulman: Set theory for category theory]. It describes some of the set theoretic issues that might occur, including your Example as Example 7.5, where he claims one needs the axiom of global choice to construct it. – Julian Kuelshammer Feb 25 '15 at 9:13
• I'm not sure what would be the meaning of constructive in this context. Perhaps a good candidate would be "Can it be done in $\sf CZF$? (or maybe $\sf IZF$?)" but this will still be missing a few things. In any case, as @Julian points out, global choice sneaks in quite easily in many places when you work with proper classes and class functions between them. – Asaf Karagila Feb 25 '15 at 9:29
• @Julian: Did you mean to include this arXiv link? – Brian M. Scott Feb 25 '15 at 9:29
• First objection: formalising what category theorists do using definable classes in ZFC is not very faithful to what we actually mean (see §6 in Shulman's paper), and sometimes there are statements which cannot even be formalised that way. Second objection: the fact that "fully faithful and essentially surjective on objects = categorical equivalence" is equivalent to the axiom of choice is, in some sense, an artifact of doing category theory in terms of set theory. No axiom of choice is needed at all if we do it in univalent foundations. Third objection: no one seriously uses anafunctors. – Zhen Lin Feb 25 '15 at 11:08
• @ZhenLin: I agree with your first objection - it's just that I would like to understand if, in principle, one could do it. So far I always thought 'Ok, it's not natural, but in theory all the maths I'm doing could be coded in $\textsf{ZFC}$' but I'm not sure about that anymore. I'd be interested in seeing an example where one cannot do this. Also, can I conclude from your comment that if you were to pick a foundational system for the formalization of mathematics, in particular category theory, you'd choose HoTT? I'd be happy if you elaborated on your thoughts in an answer. – Hanno Feb 25 '15 at 11:15

Your first observation has been fleshed out by Bénabou in his paper cited below.

My experience with category theory indicates that the answer to Question A is Yes after removing useless applications of the global axiom of choice, which is used especially in the theorem that fully faithful essentially surjective functors are equivalences. Why useless? Most equivalences of categories in practice appear as adjoint equivalences where the pseudo-inverse functor, as well as unit and counit, are already given.

It is often critized that ZFC doesn't enable us to talk about the category of all functors $\mathsf{Set} \to \mathsf{Set}$. Before moving into more sophisticated foundations (Grothendieck universes, homotopy type theory, etc.), we should first ask ourselves if it is really necessary to talk about this wild category. I would argue that ZFC is not able to formalize all of category theory, but it is able to formalize 99% of category relevant for practice.

The following papers deal with ZFC-foundations of category theory:

Feferman, Solomon, and G. Kreisel. "Set-theoretical foundations of category theory." Reports of the Midwest Category Seminar III. Springer Berlin Heidelberg, 1969.

Bénabou, Jean. "Fibered categories and the foundations of naive category theory." The Journal of Symbolic Logic 50.01 (1985): 10-37.

Shulman, Michael A. "Set theory for category theory." arXiv preprint, arXiv:0810.1279 (2008).

• I don't agree at all that ZFC alone suffices. You of all people know how convenient it is to think about very large categories like $[\mathbf{CRing}, \mathbf{Set}]$. – Zhen Lin Apr 8 '15 at 7:59
• For me it is very unconvenient to think about such a category, because many things break down. It is better to work with the category of cofinally small functors $\mathsf{CRing} \to \mathsf{Set}$. This way, set-theoretic difficulties can be avoided. – Martin Brandenburg Apr 8 '15 at 10:22
• No, that's even more inconvenient. Then all the time you have to check that things are cofinally small. It's far from obvious whether, say, the sheaf associated with a cofinally small presheaf is again a cofinally small presheaf. Even the fact that cofinally small presheaves are closed under limits requires a hard theorem. You would know all this if you actually tried to work with these things. – Zhen Lin Apr 8 '15 at 10:44