[Agda] Forget Hurken's Paradox, Agda has a quicker route to success

[Nils Anders Danielsson]

On 2012-09-06 17:21, Andreas Abel wrote:
> The problem is that Agda considers
>
>    F D = \Sigma E : Set. (D ≡ E) * (E → ⊥)
>
> as strictly positive in D.

I'm trying to understand if this is actually a problem. Are there any
dire consequences if we stick to predicative types?

> If I try the same in Coq, it is rejected because the definition of D
> is not considered strictly positiv.

How does Coq's positivity checker work? Is the usual definition of rose
trees accepted (T A = A × List (T A))?

-- 
/NAD