In 2013, a consortium of the greatest mathematicians published a massive volume which reboots our conception of mathematics. Ok, here's a rant by a frustrated

In 2013, a consortium of the greatest mathematicians published a massive volume which reboots our conception of mathematics. Ok, here's a rant by a frustrated student who's spent way too much time drinking the cool-aid. None of the authors, except for Voevodsky, is widely known among professional mathematicians. And Voevodsky is not known because of his work on HoTT. In fact, most mathematicians regard homotopy type theory as some obscure stuff logicians and computer scientists do, with no relevance to their research. And they're most certainly right. "greatest mathematicians". Nobody would call a mathematician "great" for coming up with a definition. (No, Grothendieck is not an example, because he actually put his definitions to use and solved hard problems.) Yet there are no interesting theorems proved via the univalence axiom which weren't known before. Thus, the "greatest" mathematical achievement of the HoTT community seems to have been coming up with the univalence axiom. Everybody can come up with random axioms. Thus, I'd say their greatest accomplishment is not actually mathematical but social, because they managed to market this "breakthrough" the way it has been. The whole process of how type theory research seems to work is completely absurd. Type theorists first create a syntax and later come up with a semantics for it. In other words, they first think about how they want to say something before they even know what to say. For example, the semantics of dependent Per Martin-Löf type theory were developed only 10-15 years after Martin-Löf came up with his syntax. A few years ago, somebody finally published a proof that the semantics of extensional Martin-Löf type theory is equivalent to locally cartesian closed categories (lccc's). It's not hard to understand what an lccc is, and state their defining operations/axioms. lcccs pop up everywhere. The concept of dependent types, on the other hand, has not existed in mathematics for thousands of years, seemingly without causing any harm. Nobody gained any interesting new insights by understanding dependent types, to my knowledge. Why, exactly, is this awkward axiomatization of lcccs interesting? And the same happens for intensional type theory with the univalence axiom. It's been blurted out for years that this syntax's semantics should be equivalent to infinity lcccs. Yet there is still no proof, no evidence that HoTT is the easiest axiomatization or the easiest to work with, and a proof, if it exists, will likely be extremely convoluted because it has to deal with all the peculiarities of a syntax that was created without having infinity categories in mind. A language that makes it hard to understand what it means has failed. If you don't believe me (and there is now reason why you should), please read this thread [1]. Lurie, the expert on infinity categories (well, there are others, but he's written the canonical tome), debates with type theorists about the usefulness of HoTT. I believe it ends with Lurie not seeing any usefulness and calling it a day. [1] https://mathematicswithoutapologies.wordpress.com/2015/05/13/univalent-foundations-no-comment https://mathematicswithoutapologies.wordpress.com/2015/05/13...