Can we formalise type theory intrinsically without any compromise? A case study in Cubical Agda

Tools

Chen, Liang-Ting and Nordvall Forsberg, Fredrik and Tsai, Tzu-Chun (2026) Can we formalise type theory intrinsically without any compromise? A case study in Cubical Agda. In: 15th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2026-01-12 - 2026-01-13. (https://doi.org/10.1145/3779031.3779090)

[thumbnail of Chen-etal-ACM-SIGPLAN-2025-Can-we-formalise-type-theory-intrinsically-without-any-compromise]
Preview
 Text. Filename: Chen-etal-ACM-SIGPLAN-2025-Can-we-formalise-type-theory-intrinsically-without-any-compromise.pdf
Final Published Version
License: Creative Commons Attribution 4.0 logo
Download (942kB)| Preview

Abstract

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.

ORCID iDs

Chen, Liang-Ting, Nordvall Forsberg, Fredrik ORCID logoORCID: https://orcid.org/0000-0001-6157-9288 and Tsai, Tzu-Chun;
CORE (COnnecting REpositories)