Timeline of “foundational” advances in homotopy theory?
41 comments·June 23, 2022
Because homotopy type theory is a cutting-edge area of research for type theorists and PL geeks.
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.
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.
That's not a reason, that's a definition.
I agree with you. It's the same with Category Theory. I have yet to see any practical usage of Category Theory in programming that was better than using basic algebraic reasoning and (simple) type theory.
I also find this baffling.
To be fair, the link is about homotopy theory proper (very interesting!), not homotopy type theory (a somewhat different area of study, and less interesting, in my opinion). I actually don't remember any other links about homotopy theory that weren't related to type theory. So in my view, this is a welcome development.
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.
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.
> 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...
The MO thread has almost nothing to do with homotopy type theory. It is mostly about homotopy theory in its role as a traditional topic in math. Its timeline goes all the way back to the 19th century. Algebraic geometry and topology has simply been very active subject areas the whole time. It is what a LOT of mathematicians work on, and it is probably the biggest general subject area on MO.
Frankly because I don’t get it and hope that somebody in the comments will say something that helps me to understand.
The only way to understand math like that is to do the hard work of learning by reading textbooks and other learning materials and doing exercises. Comments sections won't help you for learning this kind of advanced math.
If HoTT is what you are interested in, I recommend this single-page introduction if you are already familiar with how dependent type theory is used for theorem proving: https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes...
Sure, it'd be great if I could reach that ultimate benefit of being able to prove theorems. But if I'm being honest, I couldn't work toward that at the moment. Probably not for a while. In doing this I don't aim to get a false sense of familiarity with the actual topic. But there are a lot of tangible bite-size achievable goals in providing an opportunity for a discussion for those who understand it deeply, e.g. make a connection to something I do understand, or perhaps, observe the resolution of some tangential disagreement between domain experts, etc. :^)
"Single-page" really tricked me here.