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?