Type Theory with Single Substitutions
Ambrus Kaposi, Szumi Xie
TL;DR
This work presents a minimal single substitution calculus (SSC) for type theory, recasting type theory as a generalized algebraic theory (GAT) and avoiding parallel substitutions and B-systems. It defines SSC with core sorts $ extsf{Con}$, $ extsf{Ty}$, $ extsf{Tm}$, $ extsf{Sub}$ and operations including $p$, $q$, $[ ext{--}]$, $^+$, $oldsymbol{c}$-Pi, $ extsf{lam}$, and $ extsf{mk}/ extsf{un}$, alongside universes $ extsf{U}$ and operations $ extsf{El}$, $ extsf{Lift}$, and $ extsf{c}$; eight governing equations (four for substitutions, four for types) ensure typechecking compatibility. The paper proves that SSC-syntax is isomorphic to the traditional CwF-syntax for theories with $oldsymbol{c}$-Pi and universes, and shows how, with $oldsymbol{c}$, $oldsymbol{c}$-Σ, and universes, an SSC-model yields a CwF-model via termification; a minimised set of equations is also achievable under certain type formers. These results connect a lean, algebraic syntax to established semantic frameworks, enabling simpler model theory and formalisation (e.g., in Agda) while maintaining a robust bridge to CwF-based formulations. Overall, SSC provides a minimal, interpretable route from syntax to semantics for a broad class of type theories, with clear pathways to bootstrapping CwF structures from SSC.
Abstract
Type theory can be described as a generalised algebraic theory. This automatically gives a notion of model and the existence of the syntax as the initial model, which is a quotient inductive-inductive type. Algebraic definitions of type theory include Ehrhard's definition of model, categories with families (CwFs), contextual categories, Awodey's natural models, C-systems, B-systems. With the exception of B-systems, these notions are based on a parallel substitution calculus where substitutions form a category. In this paper we define a single substitution calculus (SSC) for type theory and show that the SSC syntax and the CwF syntax are isomorphic for a theory with dependent function space and a hierarchy of universes. SSC only includes single substitutions and single weakenings, and eight equations relating these: four equations describe how to substitute variables, and there are four equations on types which are needed to typecheck the other equations. SSC provides a simple, minimalistic alternative to parallel substitution calculi or B-systems for defining type theory. SSC relates to CwF as extensional combinatory calculus relates to lambda calculus: there are more models of the former, but the syntaxes are equivalent. If we have some additional type formers, we show that an SSC model gives rise to a CwF.