[HN Gopher] Introduction to Univalent Foundations of Mathematics...
       ___________________________________________________________________
        
       Introduction to Univalent Foundations of Mathematics with Agda
        
       Author : haltist
       Score  : 72 points
       Date   : 2023-11-11 16:26 UTC (6 hours ago)
        
 (HTM) web link (www.cs.bham.ac.uk)
 (TXT) w3m dump (www.cs.bham.ac.uk)
        
       | neovialogistics wrote:
       | I had a limited interest in exploring type theories for their own
       | sake some time ago but it receded when I was unable to resolve,
       | or find a resolution to, a conceptual problem that seems
       | extremely foundational.
       | 
       | Each type theory has a hierarchy of types: 1-types, 2-types,
       | 3.1*10^62-types, etc. but some niche type theories allow for
       | types indexed by transfinite ordinals: o-types, o+5-types, I even
       | found a construction of a theory that supports ph_a-types. There
       | is apparently at least one very counterintuitive type theory
       | where the hierarchy of indexable types provably continues past
       | the proof-theoretic ordinal of the theory, somehow, but I haven't
       | seen it myself.
       | 
       | These have real implications of what kinds of proofs you can do
       | with a given type theory.
       | 
       | .
       | 
       | The problem is deciding which of these theories to permit, or
       | possibly even deciding how to decide which theories to permit, if
       | you'll pardon the pun. I decided to give it up and get back to
       | PDEs.
        
         | turminal wrote:
         | I think this is on some level very much like deciding which
         | programming language to use. It really depends on what problems
         | you're trying to solve and there isn't a single one that is the
         | best.
         | 
         | The difference is that type theories are much less of a
         | "solved" problem and a lot of the variations are subject to
         | ongoing research. As a consequence we're still at the stage
         | where we're trying to figure out the "deciding how to decide",
         | as opposed to programming languages, where decision criteria
         | are relatively well understood.
        
       | renke1 wrote:
       | Although I had absolute no idea what I was doing when we played
       | around with Agda in university, it was kind of fun constructing a
       | few very basic proofs. It kind of felt like smashing some buttons
       | until it worked. The Emacs integration with all the Unicode
       | goodness was really something.
        
       | IngoBlechschmid wrote:
       | This is a great and well-regarded ressource!
       | 
       | If you want to experiment with Agda without installing it, you
       | can do so directly in your browser:
       | https://agdapad.quasicoherent.io/
        
       ___________________________________________________________________
       (page generated 2023-11-11 23:00 UTC)