<p>Andrej answer covers uses of extraction, but as far as <em>expressiveness</em> 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"</p>

<p>One subtle issue is <strong>induction-recursion</strong>, which gives Agda significant power and seems to be absent in Coq. However there is a <a href="http://www.cs.ru.nl/~venanzio/publications/induction_recursion.ps" rel="noreferrer">trick</a> by V. Capretta (It's likely been independently discovered) which allows expressing such definitions in Coq.</p>

CC BY-SA 4.0
2021-06-09T10:19:47.853Z
Agda's irrelevance is about judgemental equality, so talking about extraction is a misrepresentation (more directly covered by [erasure/runtime irrelevance](https://agda.readthedocs.io/en/v2.6.1.3/language/runtime-irrelevance.html#runtime-irrelevance), even though irrelevance should entail erasability). Irrelevance should give some gain in expressiveness, but not as much as impredicativity would.
mudri
CC BY-SA 3.0
2014-04-01T21:59:20.683Z
2014-04-01T21:59:20.683Z
cody
<p>Now Agda supports <code>Prop</code>: <a href="https://agda.readthedocs.io/en/v2.6.1.3/language/prop.html" rel="nofollow noreferrer">https://agda.readthedocs.io/en/v2.6.1.3/language/prop.html</a></p>
<p>However, Agda's <code>Prop</code> is <em>predicative</em> and <em>definitionally irrelevant</em>, so it's still not as strong as discussed in Cody's answer.</p>
<p>To use it, one needs to supply <code>--prop</code> to Agda. This can be done by adding <code>{-# OPTIONS --prop #-}</code> at the top of an Agda file.</p>

CC BY-SA 4.0
2021-06-08T22:54:49.280Z
2021-06-08T22:54:49.280Z
ice1000
<p>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 <a href="http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Irrelevance">Agda wiki Irrelevance page</a>.</p>

CC BY-SA 3.0
2014-03-31T06:08:04.867Z
2014-03-31T06:08:04.867Z
Andrej Bauer
<p>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? </p>

<lo.logic><dependent-type><agda>
How to use Prop from UTT in Agda
Konstantin Solomatov
# How to use Prop from UTT in Agda

(Asked by: username_0 on 2014-03-30)

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?

**Tags:** lo.logic, dependent-type, agda

---

## 3 answers

### Answer by username_4 on 2014-03-31. Score: 9 | Accepted answer

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](http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Irrelevance).


---

### Answer by username_1 on 2014-04-01. Score: 5

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](http://www.cs.ru.nl/~venanzio/publications/induction_recursion.ps) by V. Capretta (It's likely been independently discovered) which allows expressing such definitions in Coq.

> **Comments:**
> **username_2**: Agda's irrelevance is about judgemental equality, so talking about extraction is a misrepresentation (more directly covered by [erasure/runtime irrelevance](https://agda.readthedocs.io/en/v2.6.1.3/language/runtime-irrelevance.html#runtime-irrelevance), even though irrelevance should entail erasability). Irrelevance should give some gain in expressiveness, but not as much as impredicativity would.  

---

### Answer by username_3 on 2021-06-08. Score: 2

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.


---

