We give a definition of finitary type theories that subsumes many examples of dependent type theories, such as variants of Martin-L\"of type theory, simple type theories, first-order and higher-order logics, and homotopy type theory. We prove several general meta-theorems about finitary type theories: weakening, admissibility of substitution and instantiation of metavariables, derivability of presuppositions, uniqueness of typing, and inversion principles. We then give a second formulation of finitary type theories in which there are no explicit contexts. Instead, free variables are explicitly annotated with their types. We provide translations between finitary type theories with and without contexts, thereby showing that they have the same expressive power. The context-free type theory is implemented in the nucleus of the Andromeda 2 proof assistant.

翻译：我们给出了一种法系类型理论的定义,它包含许多依附类型理论的例子,例如,马丁-L\"类型理论的变体、简单类型理论、一阶和高阶逻辑以及同质理论。我们证明了关于法系类型理论的几种一般元理论:变数的削弱、替代和即时化的可接受性、预想的可衍生性、打字的独特性以及反向化原则。然后我们给出第二个法系类型理论的配方,其中没有明确的背景。相反,自由变量有明确的注释,有其类型。我们提供了有背景和没有背景的法系类型理论之间的翻译,从而表明它们具有相同的表达力。无上下文类型理论在安卓美达2号证明助理的核心实施。