[westurner]

But HoTT is removed from lean core?

From https://news.ycombinator.com/item?id=42440016#42444882 :

> /? Hott in lean4 https://www.google.com/search?q=hott+in+lean4

https://github.com/forked-from-1kasper/ground_zero :

> Lean 4 HoTT Library