Given a type system T, and a type $A$ in that type system, is there an (effective) surjection from $\mathbb{N}$ onto the set of terms of that type?
One could ask the same of set theory: isn't the set of terms that can be written down countable? Why isn't there a surjection from $\aleph_0$ to any set?

The answer, of course, is in the difference between internal truth and external truth.

Externally, the set of well typed terms of type $A$ (say in the empty context) is recursively enumerable in any reasonable type theory (like MLTT), so there is an effective surjection from $\mathbb{N}$ to that set iff it is non-empty, by a classical result in recursion theory.

Internally however, it is generally not possible to prove that such a surjection exists. In particular, a bijection between say, $\mathbb{N}$ and $\mathbb{N}\rightarrow\mathbb{N}$ implies a contradiction by a simple diagonalization argument (see, e.g., here).

In fact the proof works even if we only require a retract instead of a bijection. However this doesn't preclude a surjection from $\mathbb{N}$ to $\mathbb{N}\rightarrow\mathbb{N}$! It's only necessary that this surjection does not have a right inverse (in set theory, these right inverses always exist, but the proof of that requires the axiom of choice).

It is in fact consistent, but not provable, to assume that such a surjection exists.