Theorem provers using constructive logic have the nice property that proofs are programs; if you have a proof that A implies B, and you have an A, you can produce a B. Classical mathematics is usually based on set theory plus the axiom of choice (implying law of excluded middle), which allows non-constructive proofs (which don't compute). If the computer knows "not not X" implies "X" due to the law of the excluded middle, it can't necessarily produce an "X" from an "not not X".

The most popular theorem provers (at least among computer scientists) are based on some form of Martin-Löf type theory. In these theories, some very helpful proof techniques (often used in classical mathematics) like function extensionality and quotients don't compute. While they can be added as axioms, this breaks the computational property of the proof. What HOTT brings is a type theory with an improved notion of equality in which such things do compute, based on the notion of transport along equivalences.

If have two types

    Inductive nat : Set :=
      | O : nat
      | S : nat -> nat.

    Inductive natural_number : Set :=
      | Zero : natural_number
      | Successor : natural_number -> natural_number.

And I have proved something about nat, HOTT allows me to automatically convert that proof into a proof about natural_number (after showing nat is isomorphic to natural_number).