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

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.