3
$\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?

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

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

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