Re:Homotopy Type Theory (2012) [pdf]
by Ericson2314 on Wednesday October 28, 2020 @10:10AM
(#24918885)
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.
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.