Yes: HOTT is an acchievement. It differs from the other items on the list, though, as it belongs to the "theory building" branch of mathematics and not to the "

Yes: HOTT is an acchievement. It differs from the other items on the list, though, as it belongs to the "theory building" branch of mathematics and not to the "problem solving" branch. In the end, the current implementation of HoTT might not be the one standing the test of time; But the central idea behind the programme is here to stay: A refactoring of mathematics. (Higher) category theory is currently the best tool to uncover deep connections between different areas of mathematics. But doing higher category theory using set theory can be compared to writing a webapp directly in machine code: Possible, but cumbersome. A top level language providing suitable abstractions is needed and HoTT is one proposal. It can be compared to the ongoing shift from imperative to functional languages.