lo.logic – 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 turned out was true for benefits of standard type theory approach, these benefits require deep knowledge of the system to achieve in each instance or add more complexity than they eliminate duplication 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.