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)?
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.
But it’s indeed true that
> Understanding how things compose helps you write better APIs.
Aren’t a lot of Haskell types identical to category theory concepts? Monad?
The awesome thing about category theory is that so many things are _examples of_ category theoretic concepts. I’m sure the types you would use would be too. Then you can jump over to a different language and see the same structure.
It gives you a universal vocabulary for how things compose and interact. That’s the powerful part.
Univalence seems generally useful for verified software engineering, if we could get it in a system with regularity.
Is there a non-homotopy type theory with univalence?
Not more useful in practice than Dependent Types and/or Refinement Types. F* (F-Star) is a good example of this.
> 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...
Unfortunately I can't find the link but somewhere out there I've seen one you'd like; a radically helpful theorem prover that advertises itself as the quickest and easiest way to prove anything. The joke is that everything is true.
For those in this thread who are interested in HoTT and looking for a way in, I'll point out this series of online lectures (+ discord etc. in fact a school) beginning very soon and seemingly designed to provide that introduction. https://uwo.ca/math/faculty/kapulkin/seminars/hottest_summer...
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.
Homotopy type theory probably. Uses in modern theorem prover languages include verification of systems/hardware and formalization of math.
How can homotopy type theory, as opposed to non-homotopy type theory, help us with "verification of systems/hardware and formalization of math" outside of homotopy theory itself?
My perspective has always been that it can't.
From my experience ability to turn equivalences to equlities and vice versa is very usefull. Without this you are ending in setoid hell - intracable mess of isomorphism. I suspect that also Higher Inductive Types have lots of potential to simplify practical verification effords (apart from obvious usecases of quotients and truncations)
It is my understanding that HITs are just as easy to integrate into non-homotopy type theories as they are to HoTTs.
Homotopy is fun - not sure if I'd use it in my day to day life but its definitely entertaining in small chunks.
It's just because it's sexy.