Type theory vs. set theory is not the only choice. It is possible to combine their strengths in a new foundation: A single mathematical universe, just as in set theory, and higher-order features and abstraction, just as in type theory. Note that the listed strengths of each are the weaknesses of the other.