[TYPES] Decidable equality of propositions implies proof irrelevance

[Dominik Kirst]

Dear Types community,

studying Berardi’s 1996 proof that excluded middle (XM) implies proof irrelevance (PI) in CiC, I found that the assumption of XM can be weakened to (logically) decidable equality of propositions (DEP). Even weaker, it in fact suffices to assume a type conditional, which is definable from DEP. Has this fact been known before and is there work on related ideas? I have only found the overview of propositions independent from CiC/Coq in the Coq wiki (https://github.com/coq/coq/wiki/The-Logic-of-Coq <https://github.com/coq/coq/wiki/The-Logic-of-Coq>), where no implication from decidable equality to PI is indicated.

The proof I discovered uses Hedberg’s 1998 result to derive PI for equality proofs of propositions from DEP and then proceeds by constructing the type conditional and following the remaining structure of Berardi’s proof. If the fact DEP -> PI has been established before: what are the known proofs and, in particular, are there proofs that do not require Hedberg’s result explicitly?

Kind regards,
Dominik

-----------------------------------------
Programming Systems Lab
Saarland University
http://www.ps.uni-saarland.de/~kirst/ <http://www.ps.uni-saarland.de/~kirst/>