I understand proof irrelevance implementation as one of the two language features listed below:

  • Prop as SProp in Coq or Prop 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?

  • 2
    $\begingroup$ Regarding your second point: if you only have 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$ Commented Feb 2, 2023 at 11:12
  • $\begingroup$ Also, I feel like your title quite poorly corresponds to your question: you title mentions implementations and impredicativity, while you question does not. $\endgroup$ Commented Feb 2, 2023 at 14:26
  • 1
    $\begingroup$ @MevenLennon-Bertrand good point! I'll retitle. I have rephrased my question several times to make it better suit for the website, but I forgot to change the title correspondingly. $\endgroup$
    – ice1000
    Commented Feb 2, 2023 at 16:08


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.