You are describing types as sets, and in intensional type theory types are not sets. There is also extensional type theory, where types can be sets, but in gene

You are describing types as sets, and in intensional type theory types are not sets. There is also extensional type theory, where types can be sets, but in general we are not talking about that when we speak about type theory in connection to computer science. But regardless of ITT vs. ETT, the point of type theory is that proofs are mathematical objects. That's where the real power comes from and this is the power unityped languages lack. I suspect that this false belief that dynamically-checked language afficionados have, of types being sets, is responsible for their disdain for statically-typed languages. If you think that types are sets, it's easy to miss what they can do.