So, while type theory may have the benefit of resolving the "isomorphism issue" you describe, how is type theory not also another encoding of, for example, the real numbers?