> various versions of Martin-Löf’s intuitionistic type theory and finally the calculus of constructions of Coquand and Huet. In every case, they were created wi

> various versions of Martin-Löf’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-Löf 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-intuitionistic/#MeanExpl 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.