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

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-Notes/ https://martinescardo.github.io/HoTT-UF-in-Agda-Lecture-Note... [2] https://www.cambridge.org/core/books/introduction-to-homotopy-type-theory/0DD31EC06C80797A50ACE807251E80B6 https://www.cambridge.org/core/books/introduction-to-homotop... [3] https://github.com/HoTT-Intro/Agda https://github.com/HoTT-Intro/Agda