Reduction Free Normalisation for a proof irrelevant type of propositions
Logic in Computer Science
2024-02-14 v6
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.
Keywords
Cite
@article{arxiv.2103.04287,
title = {Reduction Free Normalisation for a proof irrelevant type of propositions},
author = {Thierry Coquand},
journal= {arXiv preprint arXiv:2103.04287},
year = {2024}
}