Some proof relevance in classical mathematics is going to be quite hard to see. While in HoTT, which proof of equality you choose may matter, it classical mathematics all proofs of equality are the same, so you won't be able to leverage them.

Take a slightly less trivial situation: proofs of $n \leq m$. Well, it turns out that the canonical such proof is (unsuprisingly) isomorphic to $m-n$. Classically, if you needed the 'content' of $n \leq m$, you'd just use $m-n$ and move on. Note that any member of $\textsf{Fin}(m-n+1)$ is a witness for $n \leq m$. The point is that the set of all proofs is $\textsf{Fin}(m-n+1)$, of cardinality $m-n+1$. If you are proof-relevant, then any of those witnesses will do, not just the "tightest" one. And your results will then depend on that choice. Because it is "too easy" to see what the best choice is, it is thus rare to not pick it.

Moving up a tiny bit more: when you say *let $X$ be a finite set of size $n$*, you definitely don't care about what is in $X$ but you might still find something odd: if you leverage all the information from the premise, in a proof-relevant setting, you get a full isomorphism between $X$ and $\textsf{Fin}(n)$; but $\textsf{Fin}(n)$ is canonically ordered, so you can induce an ordering on $X$. Which ordering? Well, the one that's in your proof! There are $n!$ such possibilities. In a classical setting, one usually assumes, silently, that you don't depend on the proof, so you assume that $X$ is unordered. [Constructively, you can't blithely assume this, which is explained very well in Brent Yorgey's PhD Thesis.] In other words, this might be a source of proof-relevance, if you're not careful! Some code I wrote for Species in Haskell ended up being accidentally proof-relevant because of exactly this.

It is worth remembering that a bijection between $\textsf{Fin}(m)$ and $\textsf{Fin}(n)$ is a witness that $m=n$. Some theorems about permutations, when de-categorified, are theorems about set cardinality. Which set isomorphism you pick matters, because it gives you a different permutation. This has non-trivial implications for reversible programming (see my work with Amr Sabry if you're curious).

My feeling is that there is in fact a lot of "proof relevant" statements in classical mathematics, they just have not yet been recognized as being such.

per se" by 'ordinary', and I'd happily count nonstandard analysis in there. $\endgroup$ – mcncm Jul 24 '20 at 19:061more comment