一句话：为支持可数宇宙层级与索引归纳-递归（IIR）类型的 Martin-Löf 类型论证明典范性，并给出将 IIR 归约到 IR 的构造。
本文为带有可数宇宙层级、且每个宇宙都支持索引归纳-递归（IIR）类型的 Martin-Löf 类型论证明 canonicity。作者分两步进行：首先利用归纳-递归（IR）类型及其他基本类型构造子构造 IIR 类型，使后续证明更简单，并说明所构造的 IIR 类型支持与 Agda 原生 IIR 实现相同的定义计算规则；其次，基于沿全局截面函子（global sections functor）的 gluing 方法，给出 IR 类型的 canonicity 证明。核心思想是用元理论中的 IIR 类型编码每个 IR 类型的 canonicity 谓词。该工作将 IIR 的 canonicity 问题归约到 IR，并扩展了 gluing 方法在依赖类型论元理论中的应用。
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.