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.

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