<div dir="ltr"><div>It's not possible to prove this in Agda because the pattern matching unification algorithm only deals with data constructors (such as 'zero' or 'suc'), not with type constructors (such as 'Nat' or 'Set'). I don't immediately see if your particular lemma here would break soundness, but that doesn't say much.</div><div><br></div><div>-- Jesper<br> </div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sat, Mar 9, 2019 at 9:57 PM Apostolis Xekoukoulotakis <<a href="mailto:apostolis.xekoukoulotakis@gmail.com">apostolis.xekoukoulotakis@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div>I don't really know the theory behind this. It simply came out in practice because of this(1)</div><div><br></div><div>Can anyone prove this? I think it is impossible to prove right now.</div><div>```<br></div><div>infix 4 _≅_<br><br>data _≅_ {ℓ1} {A : Set ℓ1} (x : A) : ∀ {ℓ2} → {B : Set ℓ2} → B → Set ℓ1 where<br>   refl : x ≅ x</div><div><br>lemma : ∀{l1 l2} → {A : Set l1} → {B : Set l2}<br>          → A ≅ B → l1 ≡ l2<br>lemma x = {!!}<br>```</div><div>Till now, I have considered levels as a nuance that I don't want to deal with.<br></div><div><br></div><div>(1) : <a href="https://github.com/agda/agda-stdlib/pull/608" target="_blank">https://github.com/agda/agda-stdlib/pull/608</a><br> </div></div></div></div>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">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>