[Agda] Strictly positive types

Nils Anders Danielsson nad at chalmers.se
Wed Aug 22 16:40:15 CEST 2012


On 2012-08-21 23:09, Andrés Sicard-Ramírez wrote:
> 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).

I don't know what constraints you are referring to. Both types have
large indices that do not "fit" in the target universe (unless Set :
Set).

-- 
/NAD



More information about the Agda mailing list