一句话：证明 Agda 风格一等宇宙层级理论的规范化、等式与类型检查可判定性，并证明层级原语可安全擦除。
在基于类型论的证明助手中，宇宙层级管理机制多样；Agda 将层级内化为类型，使其成为一等对象，并允许通过普通 Π 类型进行高阶量化。本文为受 Agda 启发、带一等宇宙层级的类型理论证明了规范化性质，以及等式判定和类型检查的可判定性。方法上，作者在 Agda 中形式化开发，并建立在以往基于外延类型语法与逻辑关系的工作之上。此外，论文证明层级原语在提取程序中可被安全擦除。这些结果为一等宇宙层级的元理论提供了机器验证的基础，也支持其在实际实现中的可靠使用。
Various mechanisms are available for managing universe levels in proof assistants based on type theory. The Agda proof assistant implements a strong form of universe polymorphism in which universe levels are internalised as a type, making levels first-class objects and permitting higher-rank quantification via ordinary Π-types. We prove normalisation and decidability of equality and type-checking for a type theory with first-class universe levels inspired by Agda. We also show that level primitives can safely be erased in extracted programs. Our development is formalised in Agda itself and builds upon previous work which uses logical relations on extrinsically typed syntax.
@article{DanielssonFK26,
title = {Normalisation for First-Class Universe Levels},
author = {Nils Anders Danielsson and Naïm Camille Favier and Ondřej Kubánek},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776645}
}