Topic: Resources for HoTT in Lean
Pier Giorgio Rayme B. (Oct 15 2021 at 18:41):
I would like to use Lean to study HoTT but I was told that I should look into Lean 2. Is that correct? Would you suggest alternatives in order to study HoTT?
Could anyone suggest some good resources (hanbooks,notes, slides or video lectures) to get into HoTT using Lean?
Thank you in advance!
Scott Morrison (Oct 15 2021 at 20:18):
I think https://github.com/gebner/hott3 is the beginning and end of HoTT in Lean3.
Sebastian Reichelt (Oct 16 2021 at 00:21):
It's not really HoTT, but includes ideas from HoTT, so it might be interesting to you: https://github.com/SReichelt/universe-abstractions/blob/main/UniverseAbstractions/Doc/UniverseAbstractions.pdf
In contrast to HoTT, this formalization replaces equality with an abstract equivalence, so that no axioms need to be added. (Univalence is incompatible with Lean >= 3 as you have noticed.) Due to the results mentioned in the introduction, it's possible to recover some of the benefits of HoTT. I think this can be taken quite far, but higher inductive types are not part of the goal (which doesn't mean that it can't be done).
Still very much WIP, but any feedback is welcome.
Pier Giorgio Rayme B. (Oct 16 2021 at 15:57):
Thank you very much! I'll take a look at that asap!
Jason Rute (Oct 16 2021 at 17:03):
You may also just want to look into Arend. It is a relatively new theorem prover using a variation of cubical type theory and good documentation/tutorials. Also, there are other theorem provers as well which are commonly used for HoTT. (Not trying to push you away from Lean. I think it is a great theorem prover, but I also realize it is quite a workaround to do HoTT in Lean.)
Floris van Doorn (Oct 17 2021 at 13:05):
HoTT has been abandoned in Lean. The biggest HoTT library in Lean is in the old version of Lean 2: https://github.com/leanprover/lean2/blob/master/hott/hott.md (and in this separate repo: https://github.com/cmu-phil/Spectral).
If you want to do HoTT, I recommend to look for a different proof assistant. There are established libraries in Coq and Agda (and separately there's Unimath). There are also various proof assistants with cubical support: (Agda, Arend and various more experimental systems).
Uranus Testing (Oct 25 2021 at 19:05):
If you are interested, I am still doing some HoTT formalizations in https://github.com/groupoid/ground.zero using the same large elimination checker as in https://github.com/gebner/hott3, so you may check out it also.
Last updated: Aug 03 2023 at 10:10 UTC