I think Cubical Type Theory (derived from HoTT) is a part of the future for general-purpose dependently-typed programming -- it has canonicity, which I'd argue is necessary for a general-purpose programming language, and it being suitable for a foundation of mathematics nigh-guarantees it's powerful enough to express whatever properties are useful in the domain.
> it has canonicity, which I'd argue is necessary for a general-purpose programming language
MLTT, even without HoTT/CTT, already features canonicity, no? (At least for positive types.)
I thought the main advantage of HoTT is that you can define non-trivial equalities, and the advantage of CTT in particular is that univalence can be derived in it (rather than introducing it as a non-computational axiom).
Right, I think I'd put univalence in my list of "I want this for my dream general-purpose dependently-typed programming language" features; being able to prove properties on simple representations of data and transport those properties to more optimized forms is pretty important, imo.
