In this episode of my continuing adventures into metametatheory, I will show how to reduce type soundness (or "subject reduction") proofs for a considerable class of dependent type theories to their sine qua non: the type correctness of the computation rules.
On the way, I'll analyse the flow of information through typing rules, making an "input/output" distinction, and the not always coincident flow of trust, making a "citizen/subject" distinction. I'll extract from this analysis a "pattern/expression" distinction for the formulae we write in typing rules and thus deliver a condition sufficient to push through all the structural cases of the type soundness proof. The notion of "residuation" which plays such a key role in confluence proofs will be central to this argument, also.
I'll sketch the road map to the typechecker which checks itself!
