[stablenode]

"Are you the high priest and decider of the usefulness of mathematics? To be honest, it almost sounds like some category theorist was super mean to you..."

Interesting and totally not ad hominem response... I believe Kevin Buzzard (an actual mathematician) had a few words about this last year: https://youtu.be/Dp-mQ3HxgDE?t=1039

[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.

[feanaro]

Given the tone of the poster who this reply was for, it seems entirely warranted.

[stablenode]

feanaro: fine, if you think so.

I find it interesting that actual mathematicians working in Category Theory, such as Tom Leinster (who wrote a lovely little introductory text on Category Theory [not covering monads though] and made it freely available on arXiv: https://arxiv.org/abs/1612.09375) are able to engage in polite discussion about the contentious viewpoints on the use of CT without resorting to personal attacks (see 2-3 minutes from his talk from a few years back: https://youtu.be/UoutGluNVlI?t=410) ... which stands in sharp contrast to some of the evangelists, whose attitude in response to criticism often reeks of arrogance and puts people off taking CT seriously, which I think is a great shame.