Hi,<br><br>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><br>Thanks,<br><br>-- <br>Andrés<br><br>