Working category theorist here. I wouldn't subscribe to that statement in this strong form, even though I am convinced that various flavors of type theory are a

Working category theorist here. I wouldn't subscribe to that statement in this strong form, even though I am convinced that various flavors of type theory are a better foundation for mathematics. But this feature doesn't make me despise ZF set theory. In fact, ZF set theory is a beautifully elegant theory. I love it for studying sets. It's just not my favorite foundation. Additionally to the reasons listed by my siblings, many important results in category theory cannot be adequately formalized in ZF for size reasons. Too often, we have to or want to deal with results concerning categories which are too big to fit into sets (these collections are called "proper classes"). In ZF, we can often only formalize specific instances of our theorems but not the general theorem itself. This is explained in more detail by Mike Shulman here: https://arxiv.org/abs/0810.1279 https://arxiv.org/abs/0810.1279 Among other partial solutions, one is to extend ZF to a theory called ZFC/S where S is a very useful mathematical fiction came to live.