# Proof of symmetry of universe-polymorphic Leibniz equality in Agda

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?

• Leibniz's equality is relying on impredicativity in an essential way. So I wouldn't be surprised if this turns out that it cannot be made to work satisfactorily.
– Trebor
Apr 2, 2022 at 14:03
• I suspect you can do this for types with decidable equality using booleans. I don't know the Agda for it but in Coq forall P, Is_true (P x) (P y). Apr 2, 2022 at 17:23

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)