Reduction Free Normalisation for a proof irrelevant type of propositions
Thierry Coquand
TL;DR
The paper addresses normalization and decidability of convertibility for a dependent type theory with a cumulative universe hierarchy $\mathsf{U}_0,\mathsf{U}_1,\dots$ where $\mathsf{U}_0$ is impredicative and proof-irrelevant, closely aligned with Lean's core. It introduces a reduction-free, Artin glueing-based normalization model $M^*$ built from an arbitrary base model $M$, and proves that the quotient map $\mathsf{Term}(\Gamma,A)\rightarrow\mathsf{Elem}(\Gamma,A)$ has a section in the initial term model $M_0$, yielding normalization and decidability of conversion and type-checking. The construction relies on a category of telescopes, a presheaf topos $\hat{\mathcal{C}}$, and an internal, glued framework that handles quotes/reflections and a special $0$ for proof-irrelevant propositions; it also proves injectivity of constructors and decidability of equality in the initial model. The work extends to dependent sums and inductive types, and hints at extending the technique to proof-relevant impredicative propositions via related follow-up work, providing a modular approach with potential impact on Lean-like type systems and proof assistants.
Abstract
We show normalisation and decidability of convertibility for a type theory with a hierarchy of universes and a proof irrelevant type of propositions, close to the type system used in the proof assistant Lean. Contrary to previous arguments, the proof does not require explicitly to introduce a notion of neutral and normal forms.