My non-expert take is the main benefits of HoTT outside of homotopy theory are related to isomorphism invariance. Specifically,
- in many dependent type theories (but not in Lean's), all constructions are automatically isomorphism-invariant in a specific sense, and
- the univalence axiom internalizes this fact, in that more or less generic proofs of isomorphism invariance follow from this axiom.
So at the most basic level, consider some property defined on some algebraic structure, e.g. whether a group is simple. If you can formalize this property in a HoTT-compatible system, then you know that it is invariant under group isomorphism, and univalence yields a trivial proof within the system, as follows: Univalence implies that isomorphic groups are equal, and then the specific proof of isomorphism invariance is given by just rewriting along that equality.
You could argue that proofs of isomorphism invariance are mathematically trivial anyway. I can see three reasons why we still want them to be one-liners (though I would love to hear opinions from people with practical experience):
- Surely, the size of such proofs depends on the complexity of the mathematical objects involved. So the benefit should increase with that complexity.
- Automation which works for simple cases can fail to handle more complex cases, whereas "isomorphism is equality" works unconditionally. (There are different ways of making that precise.)
- Isomorphism invariance is really just a special case of transporting a construction along an isomorphism. There is a generalized form of rewriting (called "path induction" in HoTT) that is appropriate for arbitrary types, not just for propositions like "a group is simple" above. For example, one might want to transport a construction along an equivalence of categories, to obtain theorems about one of the constructions "for free" from the other. There are two caveats, though:
- In "Book HoTT", where univalence is an axiom, rewriting along an equality obtained from univalence yields a "stuck term". Although one can prove everything there is to know about this term, it doesn't reduce by itself. (Note that this is not a problem if the term is a proof. Moreover, maybe
simp would help in Lean.)
- In HoTT, equality is generally not a proposition (in the Lean sense). Propositional truncation (
Nonempty in Lean) is not helpful for the more general form of rewriting, so HoTT and non-HoTT libraries are incompatible at a rather fundamental level.
There are proposed solutions to the problems mentioned above, and of course there are in fact some libraries based on different flavors of HoTT, but a direct comparison is difficult because of this incompatibility.
However, let me point out a specific situation in Lean where HoTT would make an immediate difference. In Lean, if two types neither are equal by definition nor have different cardinality, their equality is (usually?) independent. As a result, statements requiring equality of types tend to be avoided, as that assumption can essentially never be proved. But univalence is exactly that: a statement that allows equality of specific types to be proved.