2021/02/23 by Rafaël Bocquet, Bocquet, Rafaël, Ambrus Kaposi +3
Computer Science · Mathematics · #FOS: Computer and information sciences #Homotopy and Cohomology in Algebraic Topology #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.2102.11649
openalex publication_date 2021/02/23 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.