>>13253665>Pure autismIt is certainly autistic, but if you're in the realm of pure mathematics or anything remotely academic, you're already autistic. Autistic isn't a good argument against something.
> it seems like the people working on it are mostly computer scientists and a few philosohpersNo, it's mostly mathematicians and computer scientists. I mean, you have people like Bauer with a "math background" (ie a math PhD). I don't see how or why this is relevant though unless you're trying to say computer science bad.
>It's literally all the same shit. Just finding different axioms and notations for doing the same shit that set theory/logic already do.This misconception is always pushed by people outside the field. Set theory isn't incompatible with any type theories, as type theories view sets as a monotyped theory in the first place.
Type theories are important for foundations of math, absolutely, but there's this idea that we don't get anything practical or interesting outside the foundations. This was already wrong by the time homotopy was introduced in the literature, but it's wrong even now: the most "mundane" useful work you get out of this is being able to instantly and efficiently make generic code over "isomorphic" data/representation without having to deal with any sort of idea of OOP/dev autism. You get to import very sophisticated reasoning to a computational setting, which is absolutely exciting.
If we're talking about exciting mathematics, this is largely up to taste. If you find things like compactness or Fubini's theorem interesting but Hopf fibrations or higher inductive types boring, there isn't much to say. As someone who thinks both sides are interesting and not at odds with each other, you don't make much sense to me.
Having serious disdain for other branches of math seems weird to me. You see this a lot with analysts and combinatorics. Or analysts and algebra. Maybe analysts are the problem.
