There are numerous advantages to having a complete categorical or type-theoretic foundations of mathematics, especially one as constructive as HoTT. The main ad

There are numerous advantages to having a complete categorical or type-theoretic foundations of mathematics, especially one as constructive as HoTT. The main advantages in my areas of research would be that proofs in "higher-category theory" would become less cumbersome. Many set-theoretic proofs in this area are non-informative because they are are messy and opaque. This is the real promise offered by any alternative theory or explanation: insight. Besides the immediate usefulness: if "all HoTT does is give a theory that's mutually interpretable with ZFC", then holy shit what an accomplishment! You seem to have a fundamental misunderstanding about the nature of mathematical research. Most fields of research do nothing but "give a theory that's mutually interpretable" with some other field, or at least did so initially.