Another two pages with worthwhile information on the HoTT book are  and .
The point is that it makes it much more realistic to check complicated math using computers, which will become more important as math inevitably gets more complicated.
Oh, and it happens to be a functional programming language. Which says something about functional programming.
Specifically, it's (almost exactly) the Calculus of Constructions (http://en.wikipedia.org/wiki/Calculus_of_constructions), the language at the top of the lambda cube (http://en.wikipedia.org/wiki/Lambda_cube).
If you erase types, the underlying programming language is the lambda-calculus, familiar to every programmer.
Really, Martin-Loef type theory is the mathematics foundation, and the Calculus of Constructions is the computer science foundation. HoTT ties them together.
Coq's logic isn't quite the CoC anymore: impredictivity is switched off by default, Coq has universes etc.
With this in mind, I'm not sure what Voevodsky means when he says HoTT and CoC are the same thing.
In fact, the simple parts are usually the most difficult to discover. Why? Precisely because it takes extreme genius to give simple answers to mathematical questions. Over time complicated proofs and definitions get simplified and clarified (such it was with calculus, set theory, logic, group theory, and countless other topics).
So there's no precedent to believe that current mathematics won't be simplified in the future (unless, of course, you believe that all mathematics is complicated; but then you seem to be trying to make an objective point about complexity, so we'll ignore that possibility).
In addition, experience with proof assistants and dependently typed programming would be really useful.