The two main things I find compelling about type theory as a foundation are:
- A more direct way to deal with $\infty$-groupoids.
- A closer match to how mathematicians actually talk about mathematics.
Timothy Chow's answer touches on point 1, so let me just add that personally I had a lot of trouble understanding and dealing with set theoretic definitions of $\infty$-groupoids, and find the HoTT definition natural and easy to work with.
The second one I think is pretty important. If you ask an actual mathematician whether 5 is an element of 7 or what the intersection of the Monster group and the real numbers is, they'll tell you "that question doesn't make sense!" But in set theoretic foundations those kinds of questions do make sense and have answers! In type theory the answer is "that doesn't type check," which is the slightly formal version of "that doesn't even make sense."
This sort of "type checking" is really important practically! It's like dimensional analysis and often quickly tells you when a formula is wrong or gives you a good guess as to what could possibly be true.
Even for really simple things like the set theoretic definitions of particular natural numbers, of ordered pairs, and of functions, the answer that set theory gives is not at all like the typical mathematicians intuition. But the type theoretic definitions do closely match my intuition. An ordered pair is a new type of thing and you're allowed to make an ordered pair by telling me the first entry and the second entry. A function is a new type of thing and if you tell me something in the source it tells you something in the target.