> 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).