3 explained the background

Edit 2: Maybe if I explain the origin of my question, it will make clearer what I was asking. When trying to define a semantics of DTT in a locally cartesian closed category, it seems to me that the natural approach is to define the interpretation of each type and term inductively using the corresponding categorical constructions, as in D4.4 of Sketches of an Elephant. Unfortunately, this doesn't quite work, because for instance substitition is "strict" in type theory, but pullback is only up to isomorphism in a category.

It seems that the standard way to deal with this is to first strictify the pullbacks in the lccc, e.g. by replacing its codomain fibration by a split one and maybe some additional data (people talk about "comprehension categories" and suchlike). However, looking at the direct construction that doesn't work, it seems to me that it can be interpreted meaningfully as an inductive construction acting not on types+terms, but rather on derivations of typing judgments. If that's right, it seems like one could then get a meaningful interpretation of type theory in an lccc by proving that any two derivations of the same typing judgment produce canonically isomorphic interpretations in the lccc. But that would require a notion of equivalence between derivations which is tractable (so that one can show that any equivalence of derivations gives an isomorphism in the lccc) and under which all derivations can be shown to be equivalent; hence my question.

2 attempted to clarify what I wasn't asking

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.

1

# Can a typing judgment admit essentially different derivations?

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?