[Agda] Proving equality of levels with heterogeneous equality.
Roman
effectfully at gmail.com
Sun Mar 10 11:12:48 CET 2019
Quoting an old thread:
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.
More information about the Agda
mailing list