Comment by YetAnotherNick
1 year ago
I think 99.9% of the people talking about HoTT haven't used HoTT in practice. They just see isomorphism is equivalent to equivalence(or something similar), comes up with a mental model and think this is the main contribution of HoTT, whereas isomorphism is a well studied thing even before formal set theory was a thing. HoTT gets weird and anyone who has tried any tool to prove anything in HoTT knows this, and this is the reason why it didn't got adopted even though many leading tools like lean worked hard to implement it.
Have you used it? If yes, could you elaborate? Or if you haven't, can you point to any recent source on what it's like to be using HoTT in 2024?
[1] is the only video which I would say I found any bit accessible. But to be honest even after spending days, I couldn't grok it. And in my observation, different implementations of HoTT are quite different from each other.
[1]: https://www.youtube.com/watch?v=x4cz1OgpU3M