You can build all of mathematics on type theory? I very much doubt that considering there isn't even a fully unified mathematics. There's holes that don't know

You can build all of mathematics on type theory? I very much doubt that considering there isn't even a fully unified mathematics. There's holes that don't know how to be bridged between entire subfields. So I'd be impressed if type theory really could do everything, but hey, I don't know