Total layman here, but I thought one of the areas of significance is that a language that uses it can write code that is guaranteed to be bug-free, since the type system is rich enough to be able to prove correctness (given the problem being correctly stated).
That has more to do with type theory directly. So far the lectures have been a great intro to constructive logics which while build to type theory and dependently typed languages, but that's not necessarily the thrust of HoTT.
Bug-free is a bit strong, since you can only use a dependent type-theory like HoTT to establish that a program meets its specification, but the specification might be buggy.
