As an amateur who nowadays works a lot with ZFC (but who doesn't know HoTT) and who is very interested in foundations, I don't think that learning HoTT is a waste of time, I'm sure HoTT is great and I'm glad there are people working on it. However, my time is limited, so I can't really afford to spend months going down a rabbit hole if it's not going to help me with my work. So I appreciate that you shared your experience, it was helpful in making me decide to stay focused on what I'm already doing.
Most mathematicians still wouldn't care about foundations if you came up with better foundations. It's a separate area of research from most other fields of mathematics, it's not relevant to what most of them are researching, and they just don't have any interest in it. And unlike category theory more broadly, they don't particularly benefit by studying foundations deeply. It doesn't provide any improvement to their own area of study.
Everything I've just said is completely uncontroversial among mathematicians, for what it's worth. The comment I just wrote has probably been expressed on r/math dozens of times at this point.
Yes I agree with that. Let me fix my phrasing: they still wouldn't all suddenly start researching mathematical foundations, but they might apply foundational tools to what they are doing.
Really "foundations" is a word that emphasizes the ZFC "learn and ignore" approach. The type theory / category theory approach might better be called "framing", in that it begins in the pilings below the basement but also goes all the way to the roof.
