[spekcular]

I can't comment on the CS stuff with any degree of expertise; the question was from the perspective of a mathematician wanting to know about mathematical applications. And not to pick on you, but again and again I ask category theory people to give me concrete examples, and again and again I get responses like yours, which amount to fairly vague gestures at theoretical purity. Contrast this with something like Galois theory. If an undergraduate asks me why Galois theory is important, I can point to about a half-dozen important problems (in terms of their place in the theory and in history) that are inaccessible without the concepts of Galois theory. For those problems, Galois theory not just another language or a cool way of looking at things, they are (as far as I know) intractable without it. I have never seen a category-theoretic example as compelling outside of algebraic topology and adjacent fields.

I also think it's important to point out for anyone reading that one certainly doesn't need category theory to do proof verification. Some other options, and some gripes with the Coq community along the lines of the previous paragraph, are listed here: https://xenaproject.wordpress.com/2020/02/09/where-is-the-fa....

Also, if your foundational theory doesn't allow me to (easily) define a fundamental geometric object like SU(n), then it's just a non-starter. Again, I have not been able to find a reason why we ought to endure such pain to do simple things when we already have a perfectly good foundational theory. Re: the HoTT book, it is precisely because I've looked at the book that I have these questions.