# What are the advantages of proof-relevant mathematics?

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?

• Dear user18921 : I hadn't heard the term "proof-relevant mathematics" before, and it seems interesting. One thing I fear though is that this question sounds a bit broad because it sounds like the sort of thing you could "write a book on". I'm not voting to close now, but someone may feel the same way and vote to close. Is there any way you can focus the question a little more? Thanks. – rschwieb Sep 6 '13 at 14:53
• @rschwieb, thanks for the comment. I'll try to make the question more specific if I can work out how. – goblin GONE Sep 6 '13 at 14:55
• Perhaps this link could be of interest www.math.uconn.edu/~hurley/math315/proofgoldberger.pdf – imranfat Sep 6 '13 at 15:04
• @imranfat, thanks. I've actually read that article; perhaps the most interesting point made is that different proofs of the same statement may encode fundamentally different insights. So, is that a major motivation of proof-relevant mathematics? That, distinguishing equivalent from non-equivalent insights? – goblin GONE Sep 6 '13 at 15:08
• Here's one example of the difference between proof-relevant mathematics and ordinary mathematics: the axiom of choice (formulated appropriately) is a logical tautology in proof-relevant mathematics. This actually correlates well the intuitive justification for AC: if you had a proof that $\forall x . \exists y . \phi (x, y)$ then you must have an actual construction for such $y$ in terms of $x$, i.e. a choice function! – Zhen Lin Sep 6 '13 at 17:29

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.