This is a very strange claim. Just off the top of my head, this definition of "mainstream mathematics" would exclude, for instance, Gödel's more famous theorems, a good bit of Grothendieck, some of the Bourbaki collective, and a huge amount of work from rather high profile mathematicians working today.

Yeah, perhaps you're right. I was trying to delineate what gets done in maths departments from what gets done in computer science, philosophy or other departments at universities while still falling under the umbrella of mathematics.

Stuff like type theory is rarely done in maths departments (though it sometimes is).

> "space and quantity"

That's a rather narrow view even of mainstream mathematics IMO.

You can't be serious. Homotopy theory is about shape!

The OP said homotopy type theory. Homotopy theory proper is part of algebraic topology, which is certainly part of mainstream maths.

[Edit] Sorry, I originally said "you said" when it was OP who said.