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所使用的类型体系。 与以前的论点相反,证据并不明确要求引入中性和正常形式的概念。