<br><br><div class="gmail_quote">On Tue, Aug 21, 2012 at 3:44 AM, Nils Anders Danielsson <span dir="ltr"><<a href="mailto:nad@chalmers.se" target="_blank">nad@chalmers.se</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div class="HOEnZb"><div class="h5">On 2012-08-20 18:14, Andrés Sicard-Ramírez wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Reading in Coq' Art about head type constraints (section 14.1.2.1),<br>
the following type is rejected by Coq 8.4, but it is accepted by Agda<br>
(development version):<br>
<br>
data ℕ : Set where<br>
zero : ℕ<br>
suc : ℕ → ℕ<br>
<br>
data T : Set → Set where<br>
c : T (T ℕ)<br>
<br>
Could someone explain me the motivation for rejecting the type T in<br>
Coq and/or for accepting it in Agda.<br>
</blockquote>
<br></div></div>
I don't think this kind of type should be allowed. Currently we can<br>
define<br>
<br>
data _≡_ (A : Set) : Set → Set where<br>
refl : A ≡ A,<br>
<br>
and according to Voevodsky this type is incompatible with his univalent<br>
model. (By the way, I think you can define _≡_ as above in Coq as well.)<span class="HOEnZb"><font color="#888888"><br>
<br></font></span></blockquote><div><br>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).<br clear="all"></div></div><br>-- <br>
Andrés<br><br>