*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.

This report is available in the following formats:

- PDF file
- Gzipped PDF file
- PostScript file
- Gzipped PostScript file
- PostScript file with Type 1 fonts
- Gzipped PostScript file with Type 1 fonts
- LaTeX DVI file
- Gzipped LaTeX DVI file