Resources for HoTT in Lean

Stream: new members

[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