Candidates for Substitution
Healfdene H. Goguen, James McKinna · 1997
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