1) I haven't written anything about constructive logic because I don't care for it, and other issues seemed more interesting to discuss. Further, the law of excluded middle has a robust presence in modern mathematical practice. A foundational system without LEM essentially by definition cannot replace ZFC for the purpose that ZFC is used for within modern mathematics. I understood the discussion to be about what should be used to ground mathematical practice.
2) "You have opinions about what you'd like from foundations." Not really. Rather, there are different goals one might want a foundational system to achieve, and we can discuss the merits of systems based on how well they meet our desired goals. I have already said, for example, that if your goal is the practical formalization of complex proofs, then type theory might very well be suitable for achieving that goal (as demonstrated by Lean).
My objections in this thread have always been that HoTT proponents are not always precise about what goals they want to achieve, and why they think HoTT is best for achieving them. That is true even if I don't care for the stated goals.
3) "They are dogmatic and are not the opinions of those mathematicians working on foundations. Those mathematicians are interested in constructive logic, computability, the computational meaning of mathematics, replacing sets with topological spaces, replacing sets with objects closer to mathematical practice, etc." The work you've just characterized is not mainstream within the community of mathematicians working on foundations and logic. Go look at what gets published in the Journal of Mathematical Logic, for example. It's just a sociological fact that the constructivist stuff (in particular) is somewhat niche (outside of say reverse mathematics, which is different than what you noted). The views I express are fairly widespread, though I put them a bit more sharply than others.
Here's a question to illustrate this point: Who at an R1 math department works primarily on the issues you mentioned? Who got hired or got tenure on the basis of this work? I can't think of anyone off the top of my head. There are at best a few topologists who got hired for their topological work who branched out into these things later. I don't doubt that if you search you can find a handful of examples - but that number is going to be much smaller than the equivalent number of people doing "classical" set theory and logic.
4) What's so wrong with not wanting the univalence axiom in my foundational system? Or thinking that this axiom is in fact a negative? It's not very ontologically primitive, after all.