But note that by foundations one has atleast two different meanings. One meaning being examining the consistency of axioms or finding weakest set of axioms for a theorem.
The other meaning being - finding a foundation in which a given mathematical theory is naturally and easily described, analogus to designing a programming language in which the programs are easy to describe.
Most of the time in mathematics, this is done by defining high level concepts and working from there - no need to change the foundational axioms or rules of inference.
But sometimes we need more - for instance, if you read the book "Synthetic Differential Geometry", infinitesimals are naturally embedded in the theory by working in a cartesian closed category of sets. One can either embed this in ZFC using cumbersome models, or change the logic itself(remove the law of excluded middle).
The logic in HOTT deals with equality in a more careful way than the usual foundations. This is not restricted to algebraic topology alone - it certainly includes algebraic geometry and tackles a general issue which will plausibly have many more applications once the technology is available. The field of noncommutative geometry, in the style of Connes, is also about this as the problem of taking quotients is another way of the stating the issue with equality.
It is a work in progress and might take some time before bearing substantive fruit, but note that the current alternative is that any student learning higher level mathematics at the level of Lurie's books has to go through a huge amount of foundational material while the ideas themselves may not be intrinsically complicated. Instead, this complexity is an artifact of embedding the theory in current foundations like the SDG example mentioned above.
With a new foundations, there is the possibility that we can teach the material at this level to students except that there are some tweaks in foundations.