[FOM] HoTT unresponsiveness

[Joseph Shipman]

The discussion about the foundational status of Homotopy Type Theory is unproductive because the distinction I made keeps being ignored, so I will try one more time.

(1) the claim being made is that somehow HoTT is supposed to be an improvement on and a possible replacement for set theory as a foundation for mathematics in general.

(2) this is very much more dubious than the claim that HoTT is an improvement on set theory for the formalization of certain particular types or areas of mathematics.

3) the distinction between these claims keeps being fuzzed over, and the VERY SPECIFIC questions I asked to resolve this distinction keep being ignored.

4) specifically:

4a) is there any theorem in HoTT, no reasonable equivalent of which can be STATED in ZFC?
4b) is there any way in which famous theorems of ZFC such as the Prime Number Theorem or the Graph Minor Theorem or Perelman's theorem on 3-manifolds are easier to prove or understand when redone in Homotopy Type Theory?

-- JS

Sent from my iPhone