Reference. Type Theory in Type Theory using a Strictified Syntax

Ambrus Kaposi, Loïc Pujet · ICFP · 2025 · metatheory · PDF · DOI · pldb
The metatheory of dependent types has seen a lot of progress in recent years. In particular, the development of categorical gluing finally lets us work with semantic presentations of type theory (such as categories with families) to establish fundamental properties of type theory such as canonicity and normalisation. However, proofs by gluing have yet to reach the stage of computer formalisation: formal proofs for the metatheory of dependent types are still stuck in the age of tedious syntactic proofs. The main reason for this is that semantic presentations of type theory are defined using sophisticated indexed inductive types, which are prone to “transport hell”. In this paper, we introduce a new technique to work with CwFs in intensional type theory without getting stuck in transport hell. More specifically, we construct an alternative presentation of the initial CwF which encodes the substitutions as metatheoretical functions. This has the effect of strictifying all the equations that are involved in the substitution calculus, which greatly reduces the need for transports. As an application, we use our strictified initial CwF to give a short and elegant proof of canonicity for a type theory with dependent products and booleans with large elimination. The resulting proof is fully formalised in Agda.

Cite
Cite as @kaposi_pujet_2025 (helia, typst) · \cite{kaposi_pujet_2025} (LaTeX)
BibTeX
bibtex · 1 line
@article{kaposi_pujet_2025, title={Type Theory in Type Theory using a Strictified Syntax}, volume={9}, ISSN={2475-1421}, url={http://dx.doi.org/10.1145/3747535}, DOI={10.1145/3747535}, number={ICFP}, journal={Proceedings of the ACM on Programming Languages}, publisher={Association for Computing Machinery (ACM)}, author={Kaposi, Ambrus and Pujet, Loïc}, year={2025}, month=aug, pages={855–885} }
hayagriva YAML (typst)
yaml · 18 lines
kaposi_pujet_2025:
  type: article
  title: Type Theory in Type Theory using a Strictified Syntax
  author:
  - Kaposi, Ambrus
  - Pujet, Loïc
  date: 2025-08
  page-range: 855-885
  url: http://dx.doi.org/10.1145/3747535
  serial-number:
    doi: 10.1145/3747535
    issn: 2475-1421
  parent:
    type: periodical
    title: Proceedings of the ACM on Programming Languages
    publisher: Association for Computing Machinery (ACM)
    issue: ICFP
    volume: 9
Download: kaposi_pujet_2025.bib · kaposi_pujet_2025.yml
Cited by (3)

Can We Formalise Type Theory Intrinsically without Any Compromise? A Case Study in Cubical Agda chen_etal_2026CPP · 2026
We present an intrinsic representation of type theory in the proof assistant Cubical Agda, inspired by Awodey’s natural models of type theory. The initial natural model is defined as quotient inductive-inductive-recursive types, leading us to a syntax accepted by Cubical Agda without using any transports, postulates, or custom rewrite rules. We formalise some meta-properties such as the standard model, normalisation by evaluation for typed terms, and strictification constructions. Since our formalisation is carried out using Cubical Agda’s native support for quotient inductive types, all our constructions compute at a reasonable speed. When we try to develop more sophisticated metatheory, however, the ‘transport hell’ problem reappears. Ultimately, it remains a considerable struggle to develop the metatheory of type theory using an intrinsic representation that lacks strict equations. The effort required is about the same whether or not the notion of natural model is used.
PDF · DOI · pldb

Mechanizing Synthetic Tait Computability in Istari li_etal_2025CPP · 2026
Categorical gluing is a powerful technique for proving meta-theorems of type theories such as canonicity and normalization. Synthetic Tait Computability (STC) provides an abstract treatment of the complex gluing models by internalizing the gluing category into a modal dependent type theory with a phase distinction. This work presents a mechanization of STC in the Istari proof assistant. Istari is a Martin-Löf-style extensional type theory with equality reflection, which avoids much of the explicit transport reasoning typically found in intensional proof assistants. This work develops a reusable library for synthetic phase distinction, including modalities, extension types, and strict glue types, and applies it to two case studies: (1) a canonicity model for dependent type theory with dependent products and booleans with large elimination, and (2) a Kripke canonicity model for the cost-aware logical framework. Our results demonstrate that the core STC constructions can be formalized essentially verbatim in Istari, preserving the elegance of the on-paper arguments while ensuring machine-checked correctness.
PDF · DOI · arXiv · pldb

Divide and Check: Logical Relations, No Algorithms Attached poiret_etal_2026FSCD · 2026
The correctness of type-checking implementations for proof assistants based on dependent type theory relies on metatheoretical properties that ensure the decidability of typing, some of which require substantial logical strength. Recent mechanizations of such algorithms have highlighted the importance of separating the algorithmic components of the proof - often intricate but requiring relatively low logical strength - from the logical components, which depend on stronger metatheoretical properties, such as normalization or the injectivity of type constructors. In this work, we revisit the logical relations technique and show how it can be used to derive these metatheoretical properties in a direct and uniform way for a core dependent type theory featuring Π-types, N, ⊥ and a universe U. Our presentation yields a compact and conceptually simplified argument that isolates the logically strong reasoning from the algorithmic core. We argue that this approach scales smoothly to richer type theories, and demonstrate this by extending our construction to Exceptional Type Theory (ExcTT), obtaining the first mechanized canonicity proof for this theory.
DOI
Cites 57 works (7 here)
With notes (7)

Normalization for multimodal type theory gratzer-2026-normalizationLMCS · 2026
We prove normalization for MTT, a general multimodal dependent type theory capable of expressing modal type theories for guarded recursion, internalized parametricity, and various other prototypical modal situations. We prove that deciding type checking and conversion in MTT can be reduced to deciding the equality of modalities in the underlying modal situation, immediately yielding a type checking algorithm for all instantiations of MTT in the literature. This proof uses a generalization of synthetic Tait computability – an abstract approach to gluing proofs – to account for modalities. This extension is based on MTT itself, so that this proof also constitutes a significant case study of MTT.
DOI · arXiv

For the Metatheory of Type Theory, Internal Sconing Is Enough bocquet_etal_2023FSCD · 2023

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.

DOI · arXiv

First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory sterling_20212021
The implementation and semantics of dependent type theories can be studied in a syntax-independent way: the objective metatheory of dependent type theories exploits the universal properties of their syntactic categories to endow them with computational content, mathematical meaning, and practical implementation (normalization, type checking, elaboration). The semantic methods of the objective metatheory inform the design and implementation of correct-by-construction elaboration algorithms, promising a principled interface between real proof assistants and ideal mathematics. In this dissertation, I add synthetic Tait computability to the arsenal of the objective metatheorist. Synthetic Tait computability is a mathematical machine to reduce difficult problems of type theory and programming languages to trivial theorems of topos theory. First employed by Sterling and Harper to reconstruct the theory of program modules and their phase separated parametricity, synthetic Tait computability is deployed here to resolve the last major open question in the syntactic metatheory of cubical type theory: normalization of open terms.
DOI

Normalization for Cubical Type Theory sterling_angiuli_2021LICS · 2021
We prove normalization for (univalent, Cartesian) cubical type theory, closing the last major open problem in the syntactic metatheory of cubical type theory. Our normalization result is reduction-free, in the sense of yielding a bijection between equivalence classes of terms in context and a tractable language of β/η-normal forms. As corollaries we obtain both decidability of judgmental equality and the injectivity of type constructors.
Web

Gluing for Type Theory GluingForTypeTheoryFSCD · 2019
The relationship between categorical gluing and proofs using the logical relation technique is folklore. In this paper we work out this relationship for Martin-Löf type theory and show that parametricity and canonicity arise as special cases of gluing. The input of gluing is two models of type theory and a pseudomorphism between them and the output is a displayed model over the first model. A pseudomorphism preserves the categorical structure strictly, the empty context and context extension up to isomorphism, and there are no conditions on preservation of type formers. We look at three examples of pseudomorphisms: the identity on the syntax, the interpretation into the set model and the global section functor. Gluing along these result in syntactic parametricity, semantic parametricity and canonicity, respectively.
DOI

Observational equality, now! altenkirch-2007-observationalPLPV · 2007
DOI

Syntax and semantics of dependent types Hofmann_1997Semantics and Logics of Computation · 1997
DOI
External (50)
kaposi_pujet_2025 reference entries/refs/kaposi_pujet_2025/kaposi_pujet_2025.hel