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