Practical Benefits of HTT/univalent foundations for assisted proofs I'm trying to understand what the claimed practical benefits of HTT/univalent foundations are  for doing computer assisted proofs and while I've seen a lot of claims of benefits they all seem to be spelled out in a way that requires learning HTT/univalent to evaluate.  I'd like to know if it really has much of practical value to add to computer assisted proofs before I spend the time digging into a bunch of category theory to learn it.   So could someone please spell out these benefits in a way that doesn't require learning a bunch of category theory to understand and, ideally, which brings it down to what kind of benefits in end-user interface/automation we should expect these new techniques to enable?

Just for context/clarification let me explain that I read similar claimed benefits for the type theory (Curry–Howard) based approach and after a bunch of time learning enough to understand what was going on they weren't that impressive and there were drawbacks as well.  Are the benefits of HTT/univalent just more stuff like using Curry–Howard to construct proofs: kinda elegant and neat but actually not something someone interested just in efficently formalizing  classical proofs about impredicative structures which all live inside ZFC would care about? Or does it really have benefits which promise to increase the ability to enter math in a natural fashion by mathematicians doing normal math?
For instance, are the claims suggesting that this lets one reuse the same proof in multiple contexts (I assume this is meant to solve the choice of representation issues when doing math in Coq) just a theoretical niceity or is it plausible this allows the computer to do all the work under the hood?  I mean if, as it seems for many benefits claimed for the standard type theory approach, these benefits require deep knowledge of the system to achieve in each instance or add more complexity than they eliminate via deduplication they aren't so helpful.
For concreteness, one of the places I ran into discussions of the benefits of HTT/univalent is Escardo - Computing an integer using a Grothendieck topos (you have to scroll down a bit) but this is just one example but I often see somewhat vague statements suggesting this is the right or best way to formalize math with an explanation that involves colimits, sheafs, Grothendieck universes or other stuff I don't understand.  Also, this answer to a question on HTT was nice but  I don't know if that actually means the computer can (or even might in the future) efficently translate work entered in one context to another without carefully setting things up that way before entering the proof or human hinting.
 A: You didn't specify exactly what "claimed benefits" for non-univalent type theory in general you're referring to, and I happen to believe that even non-univalent type theory does have substantial benefits for the formalization of mathematics.  So let me start by recapping those, not to defend type theory in general, but because some of the benefits of univalent type theory expand on them.
One of these benefits is explained eloquently by Andrej Bauer in his answer to the question linked by LSpice in the comments: namely, since mathematics as it is done by mathematicians is essentially typed, and type theory has much more robust error-detection, whether or not the foundational kernel of your proof assistant is type theory, the vernacular that you actually use will almost inevitably be a form of type theory; and in that case why bother putting a layer of set theory under it?
Another benefit of a type-theoretic proof assistant is that type theory has many models, so that a proof formalized in (constructive) type theory actually proves much more than an analogous proof formalized in ZFC.  This is where things like categories, sheaves, and so on generally enter the picture, but the basic point can be appreciated without any of those words.  For example, instead of interpreting "type" as "set", one can additionally interpret "type" as "topological space", and the same theorems and proofs will be valid.  (Technically, he textbook definition of "topological space" isn't quite nice enough for this to be precisely true, but there are well-known modifications of it that are.)  Thus, when you prove something in type theory, you haven't just proven the theorem about sets that you would have proven in the analogous ZFC proof, but you've also proven a theorem about topological spaces at the same time.  For instance, your theorem about groups is automatically also a theorem about topological groups.  My paper The logic of space is an introduction to type theory (including univalence) from this perspective.
So what about univalent type theory?  Like non-univalent type theory, it also has many models.  Roughly speaking, every model of univalent type theory is an "extension" of some model of non-univalent type theory, and most interesting models of non-univalent type theory can be extended to some model of univalent type theory.  But the two classes of models are not equivalent, because a given non-univalent model could be extended to more than one univalent model, and often we may want to access univalent features that depend on the choice of model.  To be sure, the difference lies entirely in the world of homotopy theory / higher category theory, so this is not presently a feature that's of much relevance to mathematicians who don't yet care about such things.  However, with the increasing importance of such "homotopification" in mathematics, it seems like a good thing to accomodate in the design of a purportedly generic proof assistant, even if it will be invisible to many of its users.
More importantly for the average mathematician, univalence also makes type theory an even closer match for ordinary mathematical practice, and hence a better vernacular for a proof assistant; and also fixes some of the traditional problems of type theory relative to set theory.
Firstly, mathematics is naturally univalent: group theorists do not distinguish between isomorphic groups, and so on.  Thus, one naturally wants a vernacular for a proof assistant that can also seamlessly replace one structure with an isomorphic one.  Plenty of work has gone into finding ways to build such invariance on top of existing set-theoretic or type-theoretic foundations, which more or less amounts to building a univalent context on top of a non-univalent one; so we may ask, in parallel with Andrej's point, once we have a univalent vernacular, why bother putting a non-univalent layer under it?
Secondly, while you didn't say what drawbacks of non-univalent type theory you have in mind, traditionally many of those drawbacks have involved the unnatural treatment of quotients.  Non-univalent type theory doesn't really have a good way to deal with quotients, leading to the introduction of things like "setoids" that look very unnatural to an ordinary mathematician.  But univalent type theory solves this problem, with a very natural presentation of quotients that has all the properties an ordinary mathematician would expect.  Similarly, impredicative notions such as powersets are often klunky to deal with in non-univalent type theory, but work much better in univalent type theory.
I should say, though, as I said in my answer to the question linked by Wowoju in the comments, that these benefits are not currently huge.  The usefulness of univalence for isomorphism-invariance, in particular, is limited in the absence of proof assistants that can actually use univalence to transfer a definition across an isomorphism automatically and compute the result, rather than forcing the user to laboriously unwind the transport to figure out the result.  Cubical Agda, and other more recent proof assistants based on cubical type theories, have the promise of behaving in this way, but we still have a lot to learn about how best to design such proof assistants and what can be done with them.  Moreover, we are still working out how to reconcile these computational features with the desired many models of type theory.  So while I believe the potential benefits are substantial, many of them are still in the future.
