> 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.
Well no, they know sort of what they have to say. Type theory is syntax-directed because this is what ensures it's mechanically automated and doesn't require any intelligence to verify.
> The concept of dependent types, on the other hand, has not existed in mathematics for thousands of years, seemingly without causing any harm.
That's what some thought about Russell's basic theory of types before the inconsistencies of set theory were properly acknowledged. And now type systems are in every major programming language that drive trillion dollar industries.
> Nobody gained any interesting new insights by understanding dependent types, to my knowledge.
What kind of insights? There are plenty of great industry and computer science insights, even if there have been no or few abstract mathematical insights yet. Also, there's a growing push to use automated theorem proving tools like Coq in mathematics because of the growing complexity of this field.
Finally, your argument that a difficult proof hasn't been found in the handful of years since HoTT began, therefore HoTT is probably invalid or useless, is frankly asinine.
Can't reply to everything here. I don't know to which extent Russel's type system influenced modern-day type systems in programming languages.
Well no, they know sort of what they have to say.
Yes, I agree. But I'd expect more from people who literally want to make formal, exact proofs viable.
Type theory is syntax-directed because this is what ensures it's mechanically automated and doesn't require any intelligence to verify.
Validity of terms in extensional dependent type theory is not decidable, but that doesn't stop people from studying this system. They could just as well study free locally cartesian closed category, but I guess it would be too obviously trivial.
Also, there's a growing push to use automated theorem proving tools like Coq in mathematics because of the growing complexity of this field.
Err... There are very few mathematicians who want to spend significant effort on this. And one of my points is that there is no reason to believe that a system based on intensional dependent type theory (e.g. Coq) is the most suitable one, except that it already exists.
Finally, your argument that a difficult proof hasn't been found in the handful of years since HoTT began, therefore HoTT is probably invalid or useless, is frankly asinine.
Why thank you. HoTT has existed for 10 years now, Martin-Löf type theory for 40, and experts in the fields about to be revolutionized are very reserved. If you think that not expecting a revolution here is asinine, I don't think we can come to an agreement.
> There are very few mathematicians who want to spend significant effort on this.
Because the tools aren't quite there yet.
> And one of my points is that there is no reason to believe that a system based on intensional dependent type theory (e.g. Coq) is the most suitable one, except that it already exists.
No one has claimed otherwise.
> If you think that not expecting a revolution here is asinine
That's not what I said. You effectively claimed that the fact that a difficult proof had not yet been found, despite many believing the equivalence, somehow entails that it won't be found. That's the asinine argument. I'm sure you're very well aware of proofs that evaded mathematicians for millenia.
Well no, they know sort of what they have to say. Type theory is syntax-directed because this is what ensures it's mechanically automated and doesn't require any intelligence to verify.
> The concept of dependent types, on the other hand, has not existed in mathematics for thousands of years, seemingly without causing any harm.
That's what some thought about Russell's basic theory of types before the inconsistencies of set theory were properly acknowledged. And now type systems are in every major programming language that drive trillion dollar industries.
> Nobody gained any interesting new insights by understanding dependent types, to my knowledge.
What kind of insights? There are plenty of great industry and computer science insights, even if there have been no or few abstract mathematical insights yet. Also, there's a growing push to use automated theorem proving tools like Coq in mathematics because of the growing complexity of this field.
Finally, your argument that a difficult proof hasn't been found in the handful of years since HoTT began, therefore HoTT is probably invalid or useless, is frankly asinine.