I think we agree that it's legitimate to motivate HoTT on the grounds of pursuing proof assistants/formalized mathematics, and that other justifications – like competing with ZFC to be a "foundation of mathematics" in the philosophical sense – are not compelling. So whether it's reasonable at all for me take issue with the HoTT hype turns on whether they're offering justifications beyond practically efficient formalization.
I read the introduction to the HoTT book again and it seems to clear to me the justifications offered there go well beyond just better proof assistants. ("Homotopy type theory also brings new ideas into the very foundation of mathematics.") This is also my experience reading HoTT-adjacent people on Twitter (John Baez, random grad students). They clearly have some, I don't know how to put this, fundamentally aesthetic concerns with set theory, and offer various arguments like the ones we agreed were bad.
I appreciate you pointing out that it is possible to make a totally reasonable case for HoTT as a research program that does not resort to such specious arguments. So I am left wondering why so many other people fail to do this.
I read the introduction to the HoTT book again and it seems to clear to me the justifications offered there go well beyond just better proof assistants. ("Homotopy type theory also brings new ideas into the very foundation of mathematics.") This is also my experience reading HoTT-adjacent people on Twitter (John Baez, random grad students). They clearly have some, I don't know how to put this, fundamentally aesthetic concerns with set theory, and offer various arguments like the ones we agreed were bad.
I appreciate you pointing out that it is possible to make a totally reasonable case for HoTT as a research program that does not resort to such specious arguments. So I am left wondering why so many other people fail to do this.