Why does HN seem to be so much more interested in homotopy theory and related fields than other fields of math? I'm not a mathematician, and my understanding is that this "area" (including algebraic geometry, algebraic topology, and related areas of mathematical logic) represents a very small proportion of what career mathematicians actually work on. Does HN just like this subject because it is trendy? Because of its reputation for being difficult? Because of perceived connections to programming (of which I believe are generally exaggerated)?
Homotopy type theory is a type theory (of the Martin-Löf variety) that combines higher inductive types and has deep connections with the univalence axiom. That's probably the main reason. Then there's also cubical type theory, which some would claim gives computational meaning to HTT.
Linear algebra stuff makes it to the front page more often than other types of math I think, so I don't know that people are more interested homotopy. Although homotopy is probably overrepresented compared to its usefulness to the average HN reader.
Probably because of homotopy type theory, yeah. Why do you think the perceived connection is exaggerated?
One thing that has always bothered me is how people say that ideas from category theory can be useful while writing Haskell code. It's technically true, but really only the most basic ideas — things which would be in the first chapter of a textbook on category theory, and which many might not even consider to be part of category theory itself. (For example, every type in Haskell is inhabited, which alone somewhat limits what you can say about it...)
And then there is also the fact that there is a huge difference between the skills and ideas that are useful for writing proofs in a theorem prover and those that are useful for writing quality software.
Also, anything having to do with homotopy type theory is even further removed from programming than regular type theory. Correct me if I'm wrong but I think that it is really only useful for helping prove theorems in homotopy theory, rather than being more generally useful for other kinds of math.
> Correct me if I'm wrong but I think that it is really only useful for helping prove theorems in homotopy theory, rather than being more generally useful for other kinds of math.
It seems a little immoral to select a foundation according to how "useful for helping prove theorems" it is...
I think a lot of concepts from category theory can be applied to every day programming in a lot of languages. Understanding how things compose helps you write better APIs.
Univalence seems generally useful for verified software engineering, if we could get it in a system with regularity.
Why more useful than non-homotopy type theory?