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
$\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$
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.
