  We give a new proof of the well-known fact that all functions $(\mathbb{N}
\to \mathbb{N}) \to \mathbb{N}$ which are definable in G\"odel's System T are
continuous via a syntactic approach. Differing from the usual syntactic method,
we firstly perform a translation of System T into itself in which natural
numbers are translated to functions $(\mathbb{N} \to \mathbb{N}) \to
\mathbb{N}$. Then we inductively define a continuity predicate on the
translated elements and show that the translation of any term in System T
satisfies the continuity predicate. We obtain the desired result by relating
terms and their translations via a parametrized logical relation. Our
constructions and proofs have been formalized in the Agda proof assistant.
Because Agda is also a programming language, we can execute our proof to
compute moduli of continuity of T-definable functions.
