Metatheorems about type theories are often proven by interpreting the syntax into models constructed using categorical gluing. We propose to use only sconing (gluing along a global section functor) instead of general gluing. The sconing is performed internally to a presheaf category, and we recover the original glued model by externalization. Our method relies on constructions involving two notions of models: first-order models (with explicit contexts) and higher-order models (without explicit contexts). Sconing turns a displayed higher-order model into a displayed first-order model. Using these, we derive specialized induction principles for the syntax of type theory. The input of such an induction principle is a boilerplate-free description of its motives and methods, not mentioning contexts. The output is a section with computation rules specified in the same internal language. We illustrate our framework by proofs of canonicity, normalization and syntactic parametricity for type theory.

翻译：类型理论的元定理通常通过将语法解释到使用范畴粘合构造的模型中证明。我们提出仅使用内部范畴化（沿全局截面函子的粘合）而非一般粘合。该内部范畴化在预层范畴内部执行，并通过外部化恢复原始粘合模型。我们的方法依赖于涉及两种模型概念的结构：一阶模型（显式语境）和高阶模型（无显式语境）。内部范畴化将展示的高阶模型转化为展示的一阶模型。利用这些，我们推导出类型理论语法的专用归纳原理。此类归纳原理的输入是无需提及语境的动机与方法描述（无样板代码），输出为具有相同内部语言指定计算规则的截面。我们通过类型理论的典范性、归一化和语法参数性证明来阐释该框架。