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