类型论的相对归纳原理
Relative induction principles for type theories
摘要：
我们提出了新的归纳原则的句法依赖类型论，我们称之为相对归纳原则。关于函子F到句法中的归纳原理的结果在F的余域上是稳定的。我们依赖于前层范畴的内部语言。为了将多个前层范畴的内部语言结合起来，我们使用了依赖右伴随和多模态类型论。范畴粘合被用来证明这些归纳原理，但它在它们的陈述中是不可见的，它们涉及一个没有上下文扩展的模型概念。作为这些归纳原理的应用实例，我们给出了一些小类型论的规范性和规范化的简短和无样板的证明，并对其他元理论结果进行了草图证明。
英文摘要：
We present new induction principles for the syntax of dependent type theories, which we call relative induction principles. The result of the induction principle relative to a functor F into the syntax is stable over the codomain of F. We rely on the internal language of presheaf categories. In order to combine the internal languages of multiple presheaf categories, we use Dependent Right Adjoints and Multimodal Type Theory. Categorical gluing is used to prove these induction principles, but it not visible in their statements, which involve a notion of model without context extensions. As example applications of these induction principles, we give short and boilerplate-free proofs of canonicity and normalization for some small type theories, and sketch proofs of other metatheoretic results.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
