Comment by zozbot234

> 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://news.ycombinator.com/item?id=40414404