[Agda] Proving equality of levels with heterogeneous equality.

[Stefan Monnier]

> 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.

I'm not surprised it's not possible, but I'm surprised by
this explanation.  I'd have thought the first reason is that

    ℓ₁ ≡ ℓ₂

is ill-typed because

    ℓ₁, ℓ₂ : Level
    (≡) : {ℓ : Level} → {A : Set ℓ} → A → A → Set ℓ

and there is no ℓ for which `Level : Set ℓ`


        Stefan