Those aren't really "big wins" though. To most mathematicians, generalizations and abstraction are only interesting insofar as they are useful, and I don't see any results there someone working in mainstream mathematics would or should care about. (Obviously the Yoneda lemma is used in algebraic topology and geometry, but that's the odd one out on your list, and you don't really need categorical language to state the interesting examples.)
Also, EETC/HoTT are basically junk, as explained in detail by Harvey Friedman in various postings on the foundations of math mailing list. We already have a perfectly good foundation for mathematics and EETC/HoTT don't improve on it in any way (and in fact are worse in many respects).
Also, EETC/HoTT are basically junk, as explained in detail by Harvey Friedman in various postings on the foundations of math mailing list. We already have a perfectly good foundation for mathematics and EETC/HoTT don't improve on it in any way (and in fact are worse in many respects).