[Hercuros]

Note that Kevin Buzzard is talking in the context of convincing "mainstream" mathematicians to use a proof assistant. He specifically clarifies somewhere (not sure where in this video, but I've seen other videos where he clarifies it) that when he talks about "proper mathematics" he is doing so in kind of a tongue-in-cheek, British way and does not mean to suggest that other kinds of mathematics are not proper (don't remember the exact wording).

In the context of that video, his comments about category theorists and type theorists make a lot of sense: type theory people and (perhaps to a more limited extent) category theory people tend to be more easily sold on using a proof assistant since the kind of mathematics they do translate more easily into current proof assistants than, say, analysis or topology.

I definitely do not think that Kevin Buzzard is suggesting that type theorists and category theorists are not doing interesting and/or useful work (after all, the proof assistant he is advocating for is based on type theory). At best, he is making a sociological observation that there is a gap between the type theory/category theory community and "mainstream" mathematicians making the widespread adoption of proof assistants in mathematics more difficult.