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