Type Theory with Single Substitutions

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.