Proposal. Shall we strictify some homotopy propositions? › Two proposals for well-adapted proof-irrelevance in UF › An equivalence between sProp and hProp [01IA]

This one was suggested to me half a decade ago by Ulrik Buchholtz. The idea is to freely extend homotopy type theory with an abstract universe sProp together with an equivalence from sProp to hProp, such that every P: sProp is definitionally proof irrelevant.

(This system is distinct from the one that simply asserts that every P: hProp is definitionally proof-irrelevant. This latter theory is far stronger and actually derives UIP (and in some formulations, equality reflection!), and is therefore inconsistent with univalence.)

The status of the proposed theory is that it is very likely conservative over Homotopy Type Theory. Rafaël Bocquet has conjectured as much, and has spent several years developing the semantic machinery that would make it possible to prove this result. But today it remains a conjecture.