Hacker News Reader

I think you missed my point. The type theory is mathematics. So saying that math in type theory is nonsense.

I'm sorry but you misunderstand the situation. Set theory, type theory and category theory can be used for metamathematics [1] whereas real analysis and number theory cannot. They are foundational theories whereas real analysis and number theory are not. The reason for the difference has to do with the expressiveness of the formal languages and how they themselves can be expressed without a prior language other than formal logic itself.

[1]. https://en.wikipedia.org/wiki/Metamathematics

[2]. https://en.wikipedia.org/wiki/Foundations_of_mathematics

I know they are foundations of mathematics. They are elements of mathematical logic. No disagreement on this.

But how they are not mathematics? They are part of mathematical logic and mathematical logic or logic in general is branch of mathematics. Do you want to say they are somehow separated from math?

They are mathematics: mathematics about mathematics is what metamathematics means.

No more nonsense than studying English in English. It is true that type theory is mathematics, but the relevant fact is that it (unlike many fields of mathematics) is suitable for studying mathematics with.

Reply on news.ycombinator.com