One of the powerful things compilers are able to do during their optimization
phase is to swap out inefficient representations for equivalent ones. For
example, in Haskell you could use a lazy list to compute a sum of numbers, but
the GHC Haskell compiler will recognize that this is equivalent to using
iteration with a temporary variable. That way, you get to program against a
simple abstraction that's easy to reason about, while your executable takes
advantage of a representation better suited to the hardware platform (and that
happens to be much harder to reason about at scale).
However, equivalences known to the compiler are mostly restricted to well
known and researched data structures, such as stream fusion for lists. You could
define your own equivalences in source code (using a pair of conversion
functions that compose to identity in either direction), but you'd have to
apply them manually, and it can get tricky to choose the right type to use in
all places in order to avoid excessive conversions.
Now let's imagine a world where you get to define "higher inductive types",
say a canonical lookup map. This type has several constructors for the various
kinds of maps: binary search, AVL, red-black, Trie, Patricia, etc. Along with
the typical data constructors, you also define an equivalence type capturing
possibly multiple conversions between these representations, where different
conversions offer varying dimensions of efficiency (i.e., time vs. memory).
What if the compiler were able to use this notion to transparently rewrite map
representations, the same way it can do today with list fusion? Meanwhile, in
your code you get to work with the construction that is simplest to reason
about (and makes proof work easier, if you are in such an environment). This
may sound just like an abstract interfaces with multiple implementations, but
it includes the freedom to choose any implementation and have the compiler
transparently substitute another as needed, without affecting the meaning of
HoTT gives us a type theoretic foundation to justify this fancy rewriting
mechanism and these richly defined types, because it promotes the notion of
equivalence to being equivalent to equality. It remains to be seen how this
will actually play out in practice, but it gives us the theoretical framework
on which to base future work.