The biggest pain point with the theory was its handling of equality, which HoTT fixes.
Ergonomically.. well it's hard to describe TBH, the easiest way to see is to just download one of these systems and try using them. You try to prove a theorem and everything just ends up taking way longer than you'd expect. Mostly because you can't gloss over small details the way mathematicians will do informally. Every small turn of phrase like "for large enough N" or "without loss of generality" can become dozens of extra lines of code.
I didn't mean to doubt your claim — my limited experience is that proof assistants are totally inscrutable, although I've been inspired by some of the Lean and Agda stuff I've been seeing lately. I just wanted to ask for your perspective, since it's probably more informed than mine!
It seems to me that if you want to formalize the small details, you will necessarily have to do something different with some of those small details, won't you? Maybe a tactic search can find a formal and rigorous proof without you having to write those dozens of extra lines by hand, but simply glossing over them seems like it would defeat the goal of formalization.
Ergonomically.. well it's hard to describe TBH, the easiest way to see is to just download one of these systems and try using them. You try to prove a theorem and everything just ends up taking way longer than you'd expect. Mostly because you can't gloss over small details the way mathematicians will do informally. Every small turn of phrase like "for large enough N" or "without loss of generality" can become dozens of extra lines of code.