Can Homotopy Type Theory be used to derive more efficient algorithms on more efficient data representations from less efficient ones?
You ask if we could derive a more efficent way to compute even? Yes, we could of course. The point however is that compilers could not.

Having a compiler automatically perform very fancy optimization techniques is a hard problem. In fact, if you ask for too much the problem may become undecidable, and for almost all interesting cases at least extremely hard. Even just asking whether two simple types are isomorphic quickly leads to open research questions.

What we have gained from HoTT is not a magic wand, but rather a formalism that provides a very good and structured way of thinking and reasoning about isomorphism, equivalence and equality in general. One can think easily enough about "small scale" notion of equivalence, for example when we focus just on one particular data structure, such as a dictionary, but it's a whole other matter to be able to talk about all notions of equivalence at the same time.

In your particular case it is easy to see what it would mean to have an equivalence between two implementations of natural numbers. But how about equivalence of large software components? Or equivalence of implementations of partial differential equation solvers? How do we even being to think about it? HoTT has an answer.