[Agda] Proving equality of levels with heterogeneous equality.

[Apostolis Xekoukoulotakis]

I don't really know the theory behind this. It simply came out in practice
because of this(1)

Can anyone prove this? I think it is impossible to prove right now.
```
infix 4 _≅_

data _≅_ {ℓ1} {A : Set ℓ1} (x : A) : ∀ {ℓ2} → {B : Set ℓ2} → B → Set ℓ1
where
   refl : x ≅ x

lemma : ∀{l1 l2} → {A : Set l1} → {B : Set l2}
          → A ≅ B → l1 ≡ l2
lemma x = {!!}
```
Till now, I have considered levels as a nuance that I don't want to deal
with.

(1) : https://github.com/agda/agda-stdlib/pull/608
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190309/be4b969d/attachment.html>