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.

翻译：我们证明了一个具有宇宙层级结构和证明无关命题类型的类型系统的归一化与可判定性，该系统与证明助手Lean中使用的类型系统高度相似。与以往论证不同，本证明无需显式引入中性项与范式概念。