>The semantics is the actual mathematical ideas going on within the head of the mathematician
I think this intuitionism in the (original) sense of Brouwer.
Martin-Löf argued for something different:
"Martin-Löf’s meaning theory of intuitionistic type theory should be understood directly and “pre-mathematically”, that is, without assuming a meta-language such as set theory."
"This meaning theory follows the Wittgensteinian meaning-as-use tradition."
I think this intuitionism in the (original) sense of Brouwer.
Martin-Löf argued for something different:
"Martin-Löf’s meaning theory of intuitionistic type theory should be understood directly and “pre-mathematically”, that is, without assuming a meta-language such as set theory."
"This meaning theory follows the Wittgensteinian meaning-as-use tradition."