Canonicity for Indexed Inductive-Recursive Types
Abstract
We prove canonicity for a Martin-Löf type theory with a countable universe hierarchy where each universe supports indexed inductive-recursive (IIR) types. We proceed in two steps. First, we construct IIR types from inductive-recursive (IR) types and other basic type formers, in order to simplify the subsequent canonicity proof. The constructed IIR types support the same definitional computation rules that are available in Agda’s native IIR implementation. Second, we give a canonicity proof for IR types, building on the established method of gluing along the global sections functor. The main idea is to encode the canonicity predicate for each IR type using a metatheoretic IIR type.
Fields of Study & Subjects
Logic
programming
and type systems
Homotopy and Cohomology in Algebraic Topology
Reasoning
and Knowledge
Publication details
- Journal / source
- Proceedings of the ACM on Programming Languages
- Publisher
- Association for Computing Machinery (ACM)
- Volume
- 10
- Issue
- POPL
- Pages
- 1241–1269
- Publication date
- 8 January 2026
- Language
- EN