命题的证明无关类型无需归约的规范化
Reduction Free Normalisation for a proof irrelevant type of propositions
AI总结：
本文证明了具有宇宙层级和证明无关命题类型的类型论的规范化与可转换性可判定性，且无需显式引入中立项与正规形式的概念。
摘要：
我们证明了一个具有宇宙层级和命题证明无关类型的类型论的规范化与可转换性可判定性，该类型论接近证明助手Lean使用的类型系统。与以往论证不同，该证明无需显式引入中立项与正规形式的概念。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
