This is a demo release of Trocq, based on standard Coq/Rocq rather than HoTT.
Support for Prop has been added together with temporary axioms for proof irrelevance and prop extensionality.
This is a demo release of Trocq, based on standard Coq/Rocq rather than HoTT.
Support for Prop has been added together with temporary axioms for proof irrelevance and prop extensionality.