Hacker News new | ask | show | jobs
by spekcular 2242 days ago
HoTT is a strictly worse foundation for mathematics than ZFC, and in the end has to end up copying a bunch of the usual constructions anyway (like defining the real numbers). So this is not convincing.

One amusing problem is discussed here: https://mathoverflow.net/questions/289711/defining-sun-in-ho....

But suppose HoTT were equally good. What compelling reason is there for a working mathematician to learn it? We already know about set theory, and it meets all of our needs.
1 comments
wisnesky 2242 days ago
Honestly; I'm not sure; I'm a working computer scientist, not a working mathematician, and I use a proof assistant (Coq) all the time to have confidence that the proofs I write are correct (and more and more this is a requirement for publication in CS conferences). I want HoTT to succeed because it would turn some the axioms I must assume in the current Coq proof assistant into theorems, with significant implications for 'proof engineering' at scale (eg, verifying an OS kernel or compiler or database). When I read the math over flow post my emotional response is gladness that I can't accidentally conflate a topological space with an infinity groupoid. Many of the HoTT researchers are mathematicians (including the late Vladimir Voevodsky); presumably, the HoTT book (which I understand is available online) can give you a better answer than I can from the perspective of a working mathematician.
link
spekcular 2241 days ago
I can't comment on the CS stuff with any degree of expertise; the question was from the perspective of a mathematician wanting to know about mathematical applications. And not to pick on you, but again and again I ask category theory people to give me concrete examples, and again and again I get responses like yours, which amount to fairly vague gestures at theoretical purity. Contrast this with something like Galois theory. If an undergraduate asks me why Galois theory is important, I can point to about a half-dozen important problems (in terms of their place in the theory and in history) that are inaccessible without the concepts of Galois theory. For those problems, Galois theory not just another language or a cool way of looking at things, they are (as far as I know) intractable without it. I have never seen a category-theoretic example as compelling outside of algebraic topology and adjacent fields.

I also think it's important to point out for anyone reading that one certainly doesn't need category theory to do proof verification. Some other options, and some gripes with the Coq community along the lines of the previous paragraph, are listed here: https://xenaproject.wordpress.com/2020/02/09/where-is-the-fa....

Also, if your foundational theory doesn't allow me to (easily) define a fundamental geometric object like SU(n), then it's just a non-starter. Again, I have not been able to find a reason why we ought to endure such pain to do simple things when we already have a perfectly good foundational theory. Re: the HoTT book, it is precisely because I've looked at the book that I have these questions.

link