<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">https://github.com/agda/agda-stdlib/pull/608</a><br> </div></div></div></div>