There has been a push recently (at least in some circles) to change the foundations of mathematics from Set Theory to Type Theory (or some kind of Category Theory, etc.)
I am interested in set theory, not as foundations, but as its own branch of math, and I'm curious how it might fit into another system. For instance, in type theory we might form the type Set of all sets, and we can continue doing set theoretic arguments with a type theory as our metatheory.
My fear is that, as I understand it, a lot of motivation in set theory comes from its place as the foundation for the rest of mathematics. If we move to type theory, will large cardinal combinatorics still be useful? Presumably different models of set theory would give rise to different Types, and the Type of reals (say) would be distinct from the set of reals internal to some (fixed) type of Sets (which would be one model internal to Type Theory). Suddenly, studying determinacy says nothing about the structure of the reals that other mathematicians are using.
Broadly, then, if we switch to a different foundational system, what will happen to set theory? Forgive me if this is a naive question, but I'm only just getting into set theory, so I don't have an understanding of what current research in the area looks like, or if there is motivation besides foundations.
Best Answer
Set theory is not just a foundation of mathematics. It is an interesting topic of study on its own accords.
Ultimately, the study of large cardinals provides you with arithmetic results. That is to say, $\operatorname{Con}(T_1)\to\operatorname{Con}(T_2)$. If you want to have the measurability of projective sets, you need to have an inaccessible cardinal. If you want $\sf AD$ to hold in $L(\Bbb R)$, you need to have many Woodin cardinals and more.
Even if mathematicians "leave set theory", these results are still foundationally important and have beauty and interest on their own. Especially because changing foundations will not change the mathematics. It will still be impossible to prove or disprove naively that the product of two c.c.c. compact Hausdorff spaces is a c.c.c. space, and if we end up in a foundations where it is possible, then we know that there is some forcing axiom (or its failure) lurking in the background.
When people talk about universes type in type theory, they just give you the axioms of what it means to be a universe. They tell you nothing about its structure. And if you have different universes of different flavour, wouldn't it be nice to have a way of studying them and what different flavours are even possible?
These people who "push to change the foundations of mathematics" are missing something quite significant. When someone working in homotopy theory says that they prefer working in HoTT rather than in set theory, they say that because the translation of statements into set theory is cumbersome. The important thing is that a translation exists.
(Type theory, by the way, is not a single thing. There's a plurality of them, and the choice of which one you're using is implicitly the choice of your proof assistant software. We currently have no means of translating proofs from LEAN to Coq, for example. Yes, we can do it ourselves, but what we're doing it just re-implementing a proof. There's no compiler that takes a proof in LEAN and compiles it into a proof in Coq, or vice versa. So the different type theories end up being somewhat disjoint "on a practical level".)
There's nothing wrong with a plurality of mathematical foundations. Set theory exists as its own research field, not just to serve others. Much like how mathematics exists as its own research field, and not just to serve as a tool for physicists and engineers.
But to your question, there is some study about set theoretic results from a categorical perspective. Formalising forcing and related techniques is possible, and some people would argue that it is somehow more natural. But then again, more natural for whom? The majority of mathematicians finds the very idea of forcing somewhat confusing, and set theorists find it very natural already.
For a type theory approach, I suspect that the result is going to be that set theory will continue to operate as it does now. Much like how number theory is not going to change anytime soon either. There will be a theorem saying that you can implement it in a foundational framework, and that's enough, we can move on now.