Sets isn’t just “a branch of mathematics”. Sets is the foundation of traditional mathematics. However it has problems (paradoxes). Type theory was invented to s

Sets isn’t just “a branch of mathematics”. Sets is the foundation of traditional mathematics. However it has problems (paradoxes). Type theory was invented to solve those problem. And most modern proof assistants are based on some variation of type theory. Type theory is in many ways much simpler than Sets: The Set axioms are built on logic. While the (Martin Loff) type theory axioms aren’t. In other words, Type theory is much simpler than Set theory. The two theories look similar at the surface level. However they are fundamentally different. Values in type theory always comes with a type. That is not the case in Set theory. It makes a huge difference to how you use the two to prove things.