In any sort of type theory, there are a bunch of rules for constructing derivations of typing judgments such as $x:A,\; y:B(x) \;\vdash\; z:C(x,y)$. (I intend to include also judgments of the form $B:\mathrm{Type}$.) It's certainly possible to get to the same typing judgment using different derivations; for instance I could introduce an unnecessary variable with weakening, then substitute any term for that variable. But it feels as though such a derivation should be "$\beta$-equivalent" to a derivation which omits the unnecessary variable and substitution. So my question is:

Is there a tractable (e.g. inductively generated) equivalence relation on derivations under which all derivations of the same typing judgment become equivalent?

Although I want the answer to be yes, I suspect that it is no, because derivations are a lot like proofs, and I know that at least in intuitionistic logic, there can be multiple "essentially distinct" proofs of a given statement. If so, could it be true for some restricted class of type theories? Can one quantify its falsity?

Edit: Apparently there was a lot of room for misinterpretation of this question! To clarify: I was only talking about type theories in which inhabitation of types is witnessed by a specified term, as in the example typing judgment I gave above. (If you think of types as propositions and terms as proofs, then the question becomes "are all ways to derive a given proof-term equivalent?" But I don't generally tend to think of types only in that way.) Neel's answer seems to say: yes, as long as the type theory satisfies cut-elimination. Whether or not a given type can be inhabited by multiple distinct terms (e.g. one proposition can admit multiple distinct proofs) is a different question.