I understand proof irrelevance implementation as one of the two language features listed below:
Prop
asSProp
in Coq orProp
in Agda. They are good for introducing impredicativity in the type theory -- you just change the PTS rules.- Irrelevance as a modality like the dot syntax in Agda. They are more flexible, because we can define the same type and choose to use it in a relevant or irrelevant way, and it can interact with other modalities in the type theory.
What are the advantages of either approaches? By that, I'm asking is there anything we can do with modality-based approach while the universe-based approach cannot, and what about the other way around?
SProp
, you can always pass an argument of a squashed relevant type, and I would say this is kind of a way to encode the fact that in this particular case you want it to be irrelevant even if in general it should not be. But this is still probably a bit less flexible than the modal approach, though. $\endgroup$