[Agda] More heterogeneous equality.

[effectfully]

> Do you know of any type theory with level polymorphism that supports a rule like that?

No, but I'm no expert. It seems to me that all we need is

    suc-inj : {α β : Level} -> suc α ≡ suc β -> α ≡ β
    suc-inj refl = refl

    -- α != β of type Level
    -- when checking that the pattern refl has type suc α ≡ suc β

because we can write

    hcong : ∀ {α β δ} {A : Set α} {B : Set β} {D : Set δ} {x : A} {y : B}
          -> (f : ∀ {γ} {C : Set γ} -> C -> D) -> x ≅ y -> f x ≅ f y
    hcong f refl = refl

    levelOf : ∀ {α} {A : Set α} -> A -> Level
    levelOf {α} _ = α

    eq : ∀ {α β} -> Set α ≅ Set β -> α ≅ β
    eq p = {!hcong levelOf p!}

and the type of the expression in the hole is

    suc (suc α) ≅ suc (suc β)

Currently we can define `eq' as

    eq : ∀ {α β} -> Set α ≅ Set β -> α ≅ β
    eq {α} {β} _ rewrite trustMe {x = α} {β} = refl

which should be enough in most cases.