Whether HoTT is a better foundation of mathematics (FOM) in the sense of being easier to use in practise is an open question. It's unclear even exactly what it means to be a better or worse FOM.
Note also that all well-known foundations, including HoTT are mutually relatively consistent, which amounts to being translatable into each other (so if you can derive a contradiction in one, then you can convert that into a contradiction in the other). However that is not so important in practice. Proof automation is most important for large scale reasoning. Indeed the Lean project was started with the explicit aim of bringing better proof automation to provers based on the Curry-Howard correspondence.
Note also that all well-known foundations, including HoTT are mutually relatively consistent, which amounts to being translatable into each other (so if you can derive a contradiction in one, then you can convert that into a contradiction in the other). However that is not so important in practice. Proof automation is most important for large scale reasoning. Indeed the Lean project was started with the explicit aim of bringing better proof automation to provers based on the Curry-Howard correspondence.