Normalization by Evaluation for Non-cumulativity

Normalization by evaluation (NbE) based on an untyped domain model is a convenient and powerful way to normalize terms to their βη normal forms. It enables a concise technical setup and simplicity for mechanization. Nevertheless, to date, untyped NbE has only been studied for cumulative universe hierarchies, and its correctness proof critically relies on the cumulativity of the system. Therefore, we are faced with the question: whether untyped NbE applies to a non-cumulative universe hierarchy? Because such a universe hierarchy is also widely used by proof assistants like Agda and Lean, this question is of practical significance. Our work answers this question positively. One important property typically induced from non-cumulativity is uniqueness : every term has a unique type. To faithfully reflect the uniqueness property, we work with a Martin-L'of type theory with explicit universe levels ascribed in the syntactic judgments. On the semantic side, universe levels are also explicitly managed, which leads to more complex semantics compared with a cumulative universe hierarchy. We prove that the NbE algorithm is sound and complete, and confirm that NbE does work with non-cumulativity. Moreover, to better align with common practice, we also show that the explicit annotations of universe levels, though technically useful, are logically redundant: NbE remains applicable without these annotations. As such, we provide a mechanized foundation with NbE for non-cumulativity.