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

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.