6
$\begingroup$

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?

Improve this question
$\endgroup$
3
  • 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$
    – Meven Lennon-Bertrand
    Feb 2 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$
    – Meven Lennon-Bertrand
    Feb 2 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
    Feb 2 at 16:08

0

Reset to default

Your Answer

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

Browse other questions tagged or ask your own question.