2026-07-22T16:47:25Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:18002 2024-03-06T11:00:50Z ddc:004 open_access

For the Metatheory of Type Theory, Internal Sconing Is Enough Bocquet, Rafaël Kaposi, Ambrus Sattler, Christian type theory presheaves canonicity normalization sconing gluing 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 and normalization for type theory. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Rafaël Bocquet and Ambrus Kaposi and Christian Sattler 2023 Is Part Of LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2023.18 urn:nbn:de:0030-drops-180029 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.18 eng https://creativecommons.org/licenses/by/4.0/legalcode