[HN Gopher] Types versus sets (and what about categories?) (2022)
       ___________________________________________________________________
        
       Types versus sets (and what about categories?) (2022)
        
       Author : matt_d
       Score  : 15 points
       Date   : 2023-08-31 21:39 UTC (1 hours ago)
        
 (HTM) web link (lawrencecpaulson.github.io)
 (TXT) w3m dump (lawrencecpaulson.github.io)
        
       | dang wrote:
       | Discussed at the time:
       | 
       |  _Types versus sets (and what about categories?)_ -
       | https://news.ycombinator.com/item?id=30697421 - March 2022 (31
       | comments)
        
       | gylterud wrote:
       | > various versions of Martin-Lof's intuitionistic type theory and
       | finally the calculus of constructions of Coquand and Huet. In
       | every case, they were created with no interpretation in mind.
       | They were justified syntactically, for example via proofs of
       | strong normalisation. Models came later.
       | 
       | Martin-Lof very explicitly discussed the denotational meaning of
       | his theories. See for instance Section 5 of the SEoP entry on
       | intuitionistic type theory.
       | 
       | https://plato.stanford.edu/entries/type-theory-intuitionisti...
       | 
       | TFA is correct that type theory is syntax, but it would be wrong
       | to think of set theory as any less syntactic to the mind of an
       | intuitionist. The semantics is the actual mathematical ideas
       | going on within the head of the mathematician. Both type theory
       | and set theory must be connected to these in order to be given
       | meaning.
        
       ___________________________________________________________________
       (page generated 2023-08-31 23:00 UTC)