> You genuinely don't know how to write a TM that implements the identity function, or is there some technicality that it fails? The inhabitants of the type `f

> You genuinely don't know how to write a TM that implements the identity function, or is there some technicality that it fails? The inhabitants of the type `forall a. a -> a` (which, by the way, in an effectful, Turing-complete language, has more inhabitants than just the identity function) aren't in one-to-one correspondence with the inhabitants of the type `nat -> nat`. I asked for an isomorphism of types, you have to give me an isomorphism of types. Or maybe you don't know what “isomorphism” means in mathematics? >> What category are you working on? > I have no idea what point you're trying to make Okay, you don't know what “isomorphism” means in mathematics. > You're still wrong if you think the CTT is "true, but false if applied to matrix functions. The CTT isn't “false if applied to matrix functions”. The CTT says nothing about functions at a type not isomorphic to `nat -> nat`. It would be like saying “SilasX is all wrong about frogs!”, when you never said anything about frogs (at least, in this discussion). > No way could a computer handle that. They only know binaries numbers, not the matrix type. I mean, come on, I gave them a different name and everything!" I write my programs in high-level programming languages, not machine language, though. The whole point to high-level programming languages is to reason in terms of their abstractions, not their possible implementations.