A proof of symmetry of Leibniz equality by Andras Kovacs

Andras Kovacs has written the following definition of Leibniz equality (source):

let Eq : {A} -> A -> A -> U
    = \{A} x y. (P : A -> U) -> P x -> P y;

Apparently, this definition relies on type-in-type, otherwise Eq will be ill-typed, because the return type is supposed to be a small type (of type U), but it is actually parameterized by A -> U which is not small.

Trying to define it in Agda in a universe polymorphic way will require an explicit level (as it cannot be inferred) and an implicit level, because we want the flexibility that the motive and the type parameter can live in different universes:

open import Agda.Primitive

Eq : ∀ j {i} → {A : Set i} → (x y : A) → Set (lsuc j ⊔ i)
Eq j {i} {A} x y = (P : A → Set j) → P x → P y

Then, Andras Kovacs did the following proofs:

let refl : {A}{x : A} -> Eq x x
    = \_ px. px;

let sym : {A x y} → Eq {A} x y → Eq y x
  = λ {A}{x}{y} p. p (λ y. Eq y x) refl;

The sym seems promising, but how does it look in Agda?

Since p : (P : A -> U ?) -> P x -> P y where ? is a level we want to know, try applying P = λ y. Eq j y x to it generates p (λ y. Eq j y x) : Eq j x x -> Eq j y x, which looks good.

But what about the ? level? Since Eq j y x : Set (lsuc j ⊔ i), ? = Set (lsuc j ⊔ i), so:

refl : ∀ j {i} {A : Set i} {x : A} → Eq j x x
refl _ _ z = z

sym : ∀ j {i} {A : Set i} → {x y : A} → Eq (lsuc j ⊔ i) x y → Eq j y x
sym j {x = x} {y = y} p = p (λ y → Eq j y x) (refl j)

Very elegant!