Reduction Free Normalisation for a proof irrelevant type of propositions

TL;DR

This paper proves normalization and decidability of convertibility in a type theory similar to Lean's, without needing explicit neutral and normal forms, simplifying the theoretical framework.

Contribution

It introduces a novel approach to normalization in a proof-irrelevant type theory without relying on explicit neutral and normal forms.

Findings

Proves normalization and decidability of convertibility.

Applicable to a type system similar to Lean.

Simplifies the normalization proof process.

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.