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
?
forall P, Is_true (P x) (P y)
. $\endgroup$