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?