[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)