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!