> Mathematics may be unique in that a proof is often just as valuable an asset (and sometimes more so) than the "fact" that it proves.
This is the HoTT point of view: a 'fact' is just a 0-truncated (or maybe I've got my indexing off) type, where all we know is whether it's inhabited (proveable) or uninhabited (unproveable). We get much more information from considering not just the bare fact itself, and not just even one particular proof of it, but the space of all possible proofs.
Also, is math really unique here? Maybe it is in the sense of having absolute proofs; but I'd imagine that, in disciplines where reproducible experiment is the substitute for absolute proof, it is also true that the experiment is often as valuable as what it establishes, and that, the more kinds of experiments (not just the more trials of the same experiment) there are to establish the same thing, the better.
Your indexing is off :) Propositions (or 'facts' as you call them) are the (-1)-types, whereas 0-types are usually referred to as sets. A way to remember this is that the path-spaces (i.e. equalities) in a set are propositions, bringing you one level down.
While you're right that "proof relevance" is one of the key features of HoTT, I don't agree that what's being described here "is the HoTT point of view". Any mathematical proof bears on techniques that may be interesting beyond the proven result itself; HoTT doesn't clarify or elucidate that, nor does it aim to.
> I don't agree that what's being described here "is the HoTT point of view".
I am no expert in HoTT, so I certainly defer to what sounds like your expertise here. I should probably have said something closer to the weaker statement "this reminds me of HoTT", which hopefully is not incorrect—although you're right that what I really had in mind was proof relevance.
The HoTT n-type stuff is orthogonal to this. Fermat's last theorem is a singleton in HoTT, so any two proofs of it are equal in the HoTT sense, but new proofs would still be considered valuable.
I am no expert in HoTT, so I should definitely defer to you here; but I thought much of the power of HoTT was the ability to analyse a whole space of proofs without collapsing them to a single proof, so I'm surprised to hear it. Is your statement an informal observation, or a proveable fact? Is it true about a wide class of propositions, or is there something special about FLT?
That statement is a provable fact. FLT is "for all positive integers a,b,c and n > 2, a^n + b^n != c^n". Equalities and disequalities on natural numbers have no interesting proofs in the HoTT sense. That is, when x,y are natural numbers, x=y is either the empty type or the unit type. Formally, if FLT is the statement of Fermat's last theorem, we have isContr(FLT), which means that FLT only contains a single point.
The issue is that the terminology that is used in HoTT is highly confusing and contradicts conventional terminology. The word "proof" is used when it would be clearer to use the word "point" or "evidence" or "witness". With conventional terminology, there clearly are multiple proofs of FLT. But, when translated into HoTT, they all correspond to the same point/evidence/witness. It's similar to how there is only a single number 3, but there are many ways to write 3, for example as 1+2. There are many ways to write down the single point in FLT, and these correspond to different ways to prove FLT, but in the HoTT sense they are all equal.
A theorem in HoTT can have multiple points. This commonly happens when it is some kind of existence statement. For instance, the theorem "there exists a number greater than 3" has infinitely many points, namely 4,5,6,etc. Or a theorem "structures A and B are isomorphic" usually has infinitely many points. That statement means "there exists an f : A -> B such that f is an isomorphism between A and B", so it has one point per isomorphism between A and B.
Fermat's last theorem is not of this type. It is simply true, and the point/evidence/witness contains no data.
This is the HoTT point of view: a 'fact' is just a 0-truncated (or maybe I've got my indexing off) type, where all we know is whether it's inhabited (proveable) or uninhabited (unproveable). We get much more information from considering not just the bare fact itself, and not just even one particular proof of it, but the space of all possible proofs.
Also, is math really unique here? Maybe it is in the sense of having absolute proofs; but I'd imagine that, in disciplines where reproducible experiment is the substitute for absolute proof, it is also true that the experiment is often as valuable as what it establishes, and that, the more kinds of experiments (not just the more trials of the same experiment) there are to establish the same thing, the better.