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?
3 Answers
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.
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$– mudriJun 9, 2021 at 10:19
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.