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