I understand proof irrelevance implementation as one of the two language features listed below:
SPropin Coq or
Propin 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?