[HN Gopher] Timeline of "foundational" advances in homotopy theory? ___________________________________________________________________ Timeline of "foundational" advances in homotopy theory? Author : pizza Score : 18 points Date : 2022-06-23 06:47 UTC (16 hours ago) (HTM) web link (mathoverflow.net) (TXT) w3m dump (mathoverflow.net) | orangea wrote: | 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)? | bm3719 wrote: | Homotopy type theory is a type theory (of the Martin-Lof | 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. | tines wrote: | Probably because of homotopy type theory, yeah. Why do you | think the perceived connection is exaggerated? | orangea wrote: | 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. | remexre wrote: | Univalence seems generally useful for verified software | engineering, if we could get it in a system with | regularity. | orangea wrote: | Why more useful than non-homotopy type theory? | klysm wrote: | 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. | jeffreyrogers wrote: | 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. ___________________________________________________________________ (page generated 2022-06-23 23:00 UTC)