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.

翻译：类型理论可被描述为广义代数理论。这自动给出了模型的概念以及作为初始模型的语法存在性，该初始模型是一种商归纳-归纳类型。类型理论的代数定义包括Ehrhard的模型定义、带族范畴（CwFs）、语境范畴、Awodey的自然模型、C-系统、B-系统。除B-系统外，这些概念均基于并行替换演算，其中替换构成范畴。本文为类型理论定义了单替换演算（SSC），并证明对于包含依赖函数空间和宇宙层级的理论，SSC语法与CwF语法是同构的。SSC仅包含单替换和单弱化，以及关联这些操作的八个等式：其中四个等式描述如何替换变量，另有四个关于类型的等式用于对其他等式进行类型检查。SSC为定义类型理论提供了相较于并行替换演算或B-系统更为简洁、极简的替代方案。SSC与CwF的关系，犹如外延组合子演算与λ演算的关系：前者具有更多模型，但两者的语法是等价的。若引入额外的类型构造子，我们证明SSC模型可导出CwF。