[v64]

Formalization of many of the ideas from HoTT are currently happening in the Agda community. [1] It's out of my wheelhouse, so I don't know the exact motivations, but Agda is apparently a better way to formalize those ideas than in Lean.

Also, there's a new textbook coming out later this year that's a more modern update to the original HoTT book [2] which also has an Agda formalization. [3]

[1] https://martinescardo.github.io/HoTT-UF-in-Agda-Lecture-Note...

[2] https://www.cambridge.org/core/books/introduction-to-homotop...

[3] https://github.com/HoTT-Intro/Agda