Candidates for Substitution

From the introduction: Context morphisms, that is to say parallel substitutions with additional typing and well-formedness information, have emerged as an important tool in the semantics and metatheory of type theories: they are the basis for categorical semantics of type theory, they yield an appealing syntax for explaining proofs under hypotheses in the informal meaning theory for type theory, and most proofs of strong normalization use context morphisms to strengthen the inductive hypothesis.Kripke term models are closed under weakening or context extension, and this is used to show the admissibility of parallel substitution. In this paper we explore a uniform proof of thinning and substitution which isolates several simple candidate-style conditions on context morphisms arising from the Kripke construction. The proof exploits the evident similarity of the properties of thinning and substitution, when considered more generally as a property of context morphisms.We study this result in the context of Pure Type Systems (PTS), introduced as a general syntactic characterisation of type theories. PTS gives a framework for showing syntactic results, such as strengthening and subject reduction, for a broad class of systems. The second author gave an informal proof of closure under substitution and thinning for Geuvers' systems using context morphisms.This observation was made in the course of a long collaboration with Randy Pollack on machine-checking the meta-theory of PTS. Indeed, their first proof of thinning for PTS, used a particular class of context morphisms, the renamings, motivated by the use of context morphisms in normalization proofs.