7
$\begingroup$

I am not an expert in type theory, so I wonder what will HoTT bring to theorem proving (ITP/ATP), compared with dependent type theory? More specially, imagine Lean is implemented using HoTT, I would appreciate it if I could know what extra feature can we get (especially the features that will affect a normal user of Lean).

Thanks for any suggestions in advance!

$\endgroup$
8
  • 1
    $\begingroup$ Imagine Lean was Lean 2... $\endgroup$
    – Trebor
    Commented Oct 6, 2023 at 10:02
  • $\begingroup$ @Trebor Ah you are right, thanks for the hint! But if I just compare Lean 2 vs Lean 4, it seems Lean 4 is more powerful, so I wonder what will HoTT bring to us? $\endgroup$
    – ch271828n
    Commented Oct 6, 2023 at 12:02
  • 1
    $\begingroup$ For non-experts, HoTT gives a uniform syntax for effective quotients and provides constructive proofs of funExt, propExt. But it's a bit funny because HoTT itself builds on axioms, and funExt/propExt/quotients can be axiomatized as well $\endgroup$
    – ice1000
    Commented Oct 6, 2023 at 13:41
  • 1
    $\begingroup$ Note one can’t just add HoTT to Lean. It would conflict with stuff like Lean’s UIP and Lean’s AC which is used liberally in mathlib and elsewhere. At least small changes to Lean would be needed. (There used to be an official HoTT version of Lean 2, but that was dropped in Lean 3.) While AC is compatible with HoTT you need a weaker version than in Lean. Also I hear from some people who have tried HoTT that they feel it is too much work for the little added benefit, but of course that is what others say about formal theorem proving in general and it probably means better tooling is needed. $\endgroup$
    – Jason Rute
    Commented Oct 8, 2023 at 11:09
  • 1
    $\begingroup$ Related questions: proofassistants.stackexchange.com/questions/794/…. proofassistants.stackexchange.com/questions/1727/…. $\endgroup$
    – Jason Rute
    Commented Oct 8, 2023 at 11:12

1 Answer 1

3
$\begingroup$

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.

$\endgroup$
5
  • $\begingroup$ Thank you for the information! $\endgroup$
    – ch271828n
    Commented Oct 6, 2023 at 23:49
  • 2
    $\begingroup$ There is some interesting discussion in section 6.2 of this paper formalizing affine schemes, specifically addressing what is gained from univalence. $\endgroup$
    – Trebor
    Commented Oct 7, 2023 at 1:32
  • $\begingroup$ @Trebor Thank you! $\endgroup$
    – ch271828n
    Commented Oct 7, 2023 at 4:07
  • 3
    $\begingroup$ Anyone thinking that proofs of isomorphism invariance are trivial is welcome to simplify Rafaël Bocquet's External univalence for second-order generalized algebraic theories to a one-liner. $\endgroup$ Commented Oct 7, 2023 at 18:30
  • $\begingroup$ On the more practical side, attempts at getting automated isomorphism invariance without univalence are Univalent Parametricity and CoqEAL. And just like Rafaël's, these are definitely non-trivial. $\endgroup$ Commented Oct 8, 2023 at 19:44

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.