[TYPES] Meaning explanations and the invalidity of the law of excluded middle

[Andrej Bauer]

Perhaps it helps to solve the following simpler exercise first:

Is there a term

G : (nat → nat) → nat

such that, for any closed term f : nat → nat, G f is a Gödel code of f ?

With kind regards,

Andrej