I assume that in hoping for an effective bijection, we run into undecidability issues, but intuitively, it seems like there should at least be a surjection from $\mathbb{N}$ to the terms of any type, since well-typed terms of type theories are essentially finite trees, the set of which has cardinality $\aleph_0$. So, given a type theory* $T$ and a (non-empty) type $A$ in that type theory, can we always construct such a surjection? If possible, I would like to get a reference describing such an algorithm, if anyone has explicitly described it.* I suppose I should specify formally what I mean by type theory, but I am not aware of any name for type theories in general, so what I mean is a system consisting of a finite number of axioms (or axiom schemas), and rules, where we say $t : T$ if any only if there is a deduction (which is a finite tree whose leaves are axioms, and whose edges are rules) with conclusion $t:T$. So, examples would be simple type theory, homotopy type theory, one of the various forms of Martin-Lof type theory, etc...This question is related to mine, but what I am asking is more general.
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?
reference request;type theory
As @cody already pointed out, you cannot hope to have such a surjection inside type theory because nat nat is always internally uncountable by Cantor's diagonalization, i.e., given any alleged surjection f : nat  (nat nat), the function  n . (f n n) + 1 is not in the image of f.Under very general assumptions the terms of all types, even uninhabited ones, are computably enumerable (or recursively enumerable in the old terminology). There is no need to exclude the empty set (an enumeration is allowed to skip). For instance, suppose that in a given type theoryThe rules of inference are computably enumerable, andIt is semidecidable whether an instance of a rule is correctly usedThen, given any type A, we can enumerate its terms by dovetailing: in parallel we semidecide for every $n$ whether $n$ encodes a derivation of a term of type A. Note however that the program so obtained (when $A$ is nat) typically will not be expressible inside the type theory. It is a fun exercise to try to do it inside type theory anyway and figure out which bit does not work. Can you tell?All type theories which we meet in practice satisfy these conditions, and so do all other formal systems that people come up with. (In fact, real-world formal systems have decidable sets of decidable rules, so clearly semidecidable as well.) That's because a formal system for which we cannot even tell whether it is being used correctly, is closer to transcedental meditation than to logic.