It is a tacit assumption of the meaning explanations that the repeated computations of canonical forms is well-founded. For example, a natural number is the result of finitely many computations of the successor function \(\s\) ended by \(0\). A computation which results in infinitely many computations of \(\s\) is not a natural number in intuitionistic type theory. (However, there are extensions of type theory, for example, partial type theory, and non-standard type theory, where such infinite computations can occur, see section 7.3. To justify the rules of such theories the present meaning explanations do not suffice.)