# What drawbacks are there to using NF(U) for category theory?

In category theory, you often run into what is known as "size" issues. That is, you run into the issue that the categories you try to define are too "big" to be sets, and so you need to use classes or even larger collections. There are a couple solutions, but one of them would be to use NF or NFU. Since they have a set of all sets, you do not need to worry about your categories being to big. Having a category of all categories which is an object of itself is no problem, for example.

My question is, are there any issues with NF or NFU that would make them problematic as a foundation for category theory. If so, what are these issues?

• The stratified comprehension axioms of NF(U) prevent many of the constructions that we usually take for granted. For example, consider a set $X$ and the set $Y$ of one-element subsets of $X$. Then there's an obvious bijection from $X$ onto $Y$, namely $x\mapsto\{x\}$. NF does not prove the existence of that bijection (or indeed of any bijection $X\to Y$) in general. Sep 5, 2017 at 0:22
• In category theory you often want size issues - it is a well-known theorem that if you have a small complete category, then it must be a preorder. So if you want to have a sensible notion of complete categories, you need to have a hierarchy of sizes, and require big categories to have all small limits (as opposed to big categories having all big limits or small categories having all small limits). That said, I haven't checked if Freyd's proof goes through in NF. It seems to depend on how exactly you write things down. Sep 5, 2017 at 1:39
• Size means something mathematically. It is not an artificial problem created by idle mathematicians to annoy people. And it is not an issue either actually. For example, all categories have a class of generators (the class of all objects) and only some of them have a set of generators. Sep 5, 2017 at 9:39
• I believe that the fact that category theory includes meaningful and important statements involving size when it is formalized in a foundational theory that requires size distinctions does not a priori preclude there also being an interesting version of category theory that is formulated in a foundational theory in which size distinctions are not similarly mandatory. (In particular, note that Freyd's theorem also fails in intuitionistic logic, and there are models with nontrivial complete small categories.) Sep 5, 2017 at 10:39
• @AndreasBlass: your comment containing "NF does not prove the existence..." is very interesting to me, partly because I am working on a problem on infinite graphs, and my methods need (or rather: become cleaner if this is done) to first replace the 'ground set' by the set of one-element subsets, whence this, and for the proofs I have been toying with alternatives to ZFC. Do you know where I could read details about this particular "NF does not prove the existence..." statement? If that's true (which I don't doubt), then I can discard NF for my purposes. Sep 16, 2017 at 17:31

• @PyRulez Well, it suggests that there might be a way of rephrasing the notion of cartesian-closedness so that it becomes less of a problem. Has anyone actually done that? The general independence of category theory from the $\in$-tricacies of membership-based set theory makes me somewhat doubtful that such a rephrasing would enable one to reproduce something much resembling standard category theory. Sep 15, 2017 at 10:07