> But I think far more mathematicians point to ZFC, not type theory, as the foundations of mathematics. That's true, but it's just as true that those same math

> But I think far more mathematicians point to ZFC, not type theory, as the foundations of mathematics. That's true, but it's just as true that those same mathematicians only care about foundations as a proof of concept, not a practical device that you might someday want to do actual math in. ZFC is plenty good enough for the former, but you need type theories - or at least structural-set theories - to enable the latter (with the sorts of sanity checks that we've come to expect in any practical formal endeavor)!