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.