4
$\begingroup$

In Ulf Norell's thesis he mentions that Agda is based on Luo's UTT. However, I can't find a way to use Prop there. Is there any way to do so?

Improve this question
$\endgroup$
8
$\begingroup$

In Agda this is done by tagging types as "irrelevant". It's a kind of quotenting. A function from an irrelevant to a (relevant) type must be constant (and Agda enforces this). You can read more about it on the Agda wiki Irrelevance page.

Improve this answer
$\endgroup$
4
$\begingroup$

Andrej answer covers uses of extraction, but as far as expressiveness goes, I believe that having impredicative Prop leads to a system that is strictly stronger than Agda. In fact "Martin-Löf type theory with universes" is sometimes called "Luo's predicative UTT"

One subtle issue is induction-recursion, which gives Agda significant power and seems to be absent in Coq. However there is a trick by V. Capretta (It's likely been independently discovered) which allows expressing such definitions in Coq.

Improve this answer
$\endgroup$
1
  • $\begingroup$ Agda's irrelevance is about judgemental equality, so talking about extraction is a misrepresentation (more directly covered by erasure/runtime irrelevance, even though irrelevance should entail erasability). Irrelevance should give some gain in expressiveness, but not as much as impredicativity would. $\endgroup$
    – mudri
    Jun 9 at 10:19
1
$\begingroup$

Now Agda supports Prop: https://agda.readthedocs.io/en/v2.6.1.3/language/prop.html

However, Agda's Prop is predicative and definitionally irrelevant, so it's still not as strong as discussed in Cody's answer.

To use it, one needs to supply --prop to Agda. This can be done by adding {-# OPTIONS --prop #-} at the top of an Agda file.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.