Substitution Without Copy and Paste

TL;DR

This work tackles the duplication inherent in mechanising substitution for calculi with binders by factorising the variable/renaming and term/substitution distinction into a two-element Sort and a single substitution operation. The Sort-based approach, together with a quotient-inductive specification (QIIT) and Agda termination tricks, yields a simply typed category with families ($CwF$) that is isomorphic to the initial $CwF$, enabling substitution normal forms and an initiality result. The paper provides a complete development, including termination proofs, laws for the substitution functor, and a constructive isomorphism between an initial CwF and a recursively defined one, plus a discussion of practical aspects and potential extensions to dependent type theory and higher coherence. The results suggest a practical, scalable method for formalising substitution in the presence of binders, with implications for interpreting dependent types in higher categories and for mechanised proofs in proof assistants beyond Agda.

Abstract

Defining substitution for a language with binders like the simply typed $λ$-calculus requires repetition, defining substitution and renaming separately. To verify the categorical properties of this calculus, we must repeat the same argument many times. We present a lightweight method that avoids repetition and that gives rise to a simply typed category with families (CwF) isomorphic to the initial simply typed CwF. Our paper is a literate Agda script.

Figures (1)

• Figure 1: Call graph of substitution operations