<div dir="ltr"><div><div><div>Do you know of any type theory with level polymorphism that supports a rule like that? I can agree that this would indeed be convenient in some cases, but we should be careful of adding new unification rules whenever it seems convenient. At least for the regular heterogeneous equality we have now, we know that the elimination rule is equivalent with K.<br><br></div>For the record, my new unifier (see other thread) reports the following:<br><br><div style="margin-left:40px">α != β of type .Agda.Primitive.Level<br>when checking that the pattern refl has type Set α ≅ Set β<br></div><br></div>I'm not sure if this is more or less understandable than the current error message. At least it doesn't talk about a "heterogeneous constraint", of which most people won't know what it means.<br><br></div><div>cheers,<br></div><div>Jesper<br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Dec 14, 2015 at 8:58 AM, effectfully <span dir="ltr"><<a href="mailto:effectfully@gmail.com" target="_blank">effectfully@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi. Agda 2.4.3 allows to define<br>
<br>
data _≅_ {α} {A : Set α} (x : A) : ∀ {β} {B : Set β} -> B -> Set where<br>
refl : x ≅ x<br>
<br>
`A' and `B' lie in different universes and the whole thing lies in<br>
`Set'. This is very convenient, but is it reliable? If so, can the<br>
definition in the standard library be replaced by this one?<br>
<br>
Agda rejects<br>
<br>
eq : ∀ {α β} -> Set α ≅ Set β -> α ≅ β<br>
eq refl = refl<br>
<br>
-- Refuse to solve heterogeneous constraint Set α : Set (lsuc α) =?=<br>
-- Set β : Set (lsuc β)<br>
<br>
Is it a natural restriction?<br>
<br>
Also, can somebody explain how Agda infers levels in data/record<br>
declarations now? Is there a paper?<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div><br></div>