What are the advantages of proof-relevant mathematics? I've read that

Theorems in HoTT (homotopy type theory) tend to characterize the space of proofs of a
  proposition, rather than simply state that the corresponding type is
  inhabited.

So, HoTT could be described as a "proof-relevant" approach to mathematics. Indeed, there seems to be a lot of excitement about proof-relevant mathematics in general, and homotopy type theory in particular.
In broad terms, what are the advantage(s) of proof-relevant mathematics, and why are people so excited about it?
In particular, does it help us answer questions that are of interest to proof-irrelevant schools of mathematics?
 A: I know this is an old question by now, but here is my two cents:
One of the reasons people care about proof-relevant mathematics is because of its computational content.
Proof-relevant mathematics allows us to treat proofs as mathematical objects themselves and, under the proposition-as-types correspondence, we can think of a proof of a proposition as a program of a type, meaning basically that you can extract code from proofs. This holds for proofs of any statements $-$ including the ones of the form $\exists x . \varphi (x)$ and $\varphi \lor \psi$ (this is closely related to Zhen Lin's comments to your question, for the code extracted from $\forall x.\exists y. \varphi (x,y)$ does indeed correspond to a choice function).
Of course, another advantage of proof-relevant mathematics is that $-$ because proofs are objects $-$ you can investigate whether or not two proofs are equal. Since you mentioned Homotopy Type Theory (HoTT), let me say that it has many potential contributions in this respect since one of its motivations is precisely the idea that two objects may be the same in more than one way.
