We propose an abstract notion of a type theory to unify the semantics of various type theories including Martin-L\"{o}f type theory, two-level type theory and cubical type theory. We establish basic results in the semantics of type theory: every type theory has a bi-initial model; every model of a type theory has its internal language; the category of theories over a type theory is bi-equivalent to a full sub-2-category of the 2-category of models of the type theory.

翻译：我们提出了一种类型论的抽象概念，以统一多种类型论（包括马丁-洛夫类型论、双层类型论和立方体类型论）的语义。我们建立了类型论语义中的基本结果：每种类型论都有一个双初始模型；每个类型论模型都有其内部语言；给定类型论上的理论范畴与该类型论模型的2-范畴的全子2-范畴是双等价的。