Proof of symmetry of universe-polymorphic Leibniz equality in Agda

Question

Consider the following definition of universe-polymorphic Leibniz equality:

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

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

Can I make the level parameter (lsuc j ⊔ i) simpler? Do I always have to use two levels?

Here is a proof of symmetry I came up with:

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)

The input equality and the output equality don't even live in the same level. Can I avoid that? Is it possible to "lift" an instance of Eq j y x to Eq (lsuc j ⊔ i) y x?

Answer 1

Here is a version where A : Set i and both equalities live in Set (lsuc i). The idea is taken from Leibniz Equality is Isomorphic to Martin-Löf identity, parametrically (it's basically a copy of their proof in section 3).

open import Agda.Primitive

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

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

sym : ∀ {i} {A : Set i} {a b : A} → Eq a b → Eq b a
sym {a = a} a=b P = a=b (λ y → P y → P a) (refl P)