[Agda] Strictly positive types

[Andrés Sicard-Ramírez]

On Tue, Aug 21, 2012 at 3:44 AM, Nils Anders Danielsson <nad at chalmers.se>wrote:

> 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.)
>
>
Yes, the type _≡_ can also be defined in Coq, but I don't see its relation
to the head type constraints (as described in the Coq'Art).

-- 
Andrés
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20120821/5f59937a/attachment.html