What are the advantages of proof-relevant mathematics?

Solution 1:

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.