You are conflating two things - the language of math, and the language of proving facts about the language of math. The former is almost entirely sets, while t

You are conflating two things - the language of math, and the language of proving facts about the language of math. The former is almost entirely sets, while the later is necessarily types.