Resources for HoTT in Lean

Stream: general

[Pier Giorgio Rayme B.]

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]

I think https://github.com/gebner/hott3 is the beginning and end of HoTT in Lean3.

[Sebastian Reichelt]

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.]

Thank you very much! I'll take a look at that asap!

[Jason Rute]

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]

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]

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.