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.
翻译:关于类型理论的元体往往通过将语法解释成使用绝对胶层构建的模型而得到证明。 我们提议只使用隐蔽( 与全球区段真菌结合) 而不是一般胶层。 隐蔽在内部进行, 我们通过外部化恢复原始粘合模型。 我们的方法依靠两种模型概念的构造: 一阶模型( 具有明确背景) 和高阶模型( 没有明确背景 ) 。 隐蔽将显示的高阶模型转换成显示的第一阶模型。 使用这些模型, 我们为类型理论的合成得出专门的诱导原则。 这种诱导原则的输入是对其动机和方法的无锅炉板描述, 不提及背景。 输出是带有相同内部语言规定的计算规则的一节。 我们用直线性、 常规化和 合成参数来说明我们的框架 。