Comment by fooker

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.