> HoTT is a highly technical, highly niche topic and it doesn't make sense to tackle two ambitious projects at the same time like this.

It's also a bit of a controversial topic in formalized mathematics. See the following relevant comments by Kevin Buzzard (an expert in Lean and also in the sort of abstract nonsense that might arguably benefit directly from HoTT) - Links courtesy of https://ncatlab.org/nlab/show/Kevin+Buzzard

* Is HoTT the way to do mathematics? (2020) https://www.cl.cam.ac.uk/events/owls/slides/buzzard.pdf ("Nobody knows because nobody tried")

* Grothendieck's use of equality (2024) https://arxiv.org/abs/2405.10387 - Discussed here https://news.ycombinator.com/item?id=40414404