[Agda] Strictly positive types

[Nils Anders Danielsson]

On 2012-08-20 18:14, Andrés Sicard-Ramírez wrote:
> Reading in Coq' Art about head type constraints (section 14.1.2.1),
> the following type is rejected by Coq 8.4, but it is accepted by Agda
> (development version):
>
> data ℕ : Set where
>    zero : ℕ
>    suc  : ℕ → ℕ
>
> data T : Set → Set where
>    c : T (T ℕ)
>
> Could someone explain me the motivation for rejecting the type T in
> Coq and/or for accepting it in Agda.

I don't think this kind of type should be allowed. Currently we can
define

   data _≡_ (A : Set) : Set → Set where
     refl : A ≡ A,

and according to Voevodsky this type is incompatible with his univalent
model. (By the way, I think you can define _≡_ as above in Coq as well.)

-- 
/NAD