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?
$\begingroup$
$\endgroup$
asked Mar 30 '14 at 21:50
Add a comment
|
$\begingroup$
$\endgroup$
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.
answered Mar 31 '14 at 6:08
$\begingroup$
$\endgroup$
1
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.
-
$\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$ – James Wood Jun 9 at 10:19
$\begingroup$
$\endgroup$
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.
