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)?
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.
I don't mean any offense to you personally, but this kind of comment is why I hate internet discussions. You just said the opposite of what I said without adding anything new.
Nope. It is just a different model for the same thing. You might find it enlightens your understanding of composition but it doesn't make it more "real" than any other model.
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.
> 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...
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.
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?
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)
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.
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.
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.
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. :^)
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.
43 comments
[ 2.1 ms ] story [ 102 ms ] threadAnd 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.
> Understanding how things compose helps you write better APIs.
https://golem.ph.utexas.edu/category/2020/01/profunctor_opti...
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.
It seems a little immoral to select a foundation according to how "useful for helping prove theorems" it is...
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...
My perspective has always been that it can't.
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.
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...