6
$\begingroup$

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?

$\endgroup$
2
  • 5
    $\begingroup$ 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. $\endgroup$
    – Trebor
    Apr 2, 2022 at 14:03
  • $\begingroup$ 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). $\endgroup$ Apr 2, 2022 at 17:23

1 Answer 1

6
$\begingroup$

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)
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.