Leibniz equality

I stumbled upon a paper that states leibniz equality is isometric to Martin-Löf identity, parametrically. Could this mean we can just skip the identity type entirely?

Leibniz equality is defined as:

(x ≡ y) = (P : A → Set) → P x → P y

Given any x and y, they're same only given any predicate P, P(x) if and only if P(y).

The paper presents that we can prove the leibniz equality to be reflexive, transitive and symmetric.

reflexive : {a : A} → (a ≡ a)
reflexive P = id

transitive : {a b c : A} → (a ≡ b) → (b ≡ c) → (a ≡ c)
transitive ab bc P = bc P ∘ ab P

symmetric : {a b : A} → (a ≡ b) → (b ≡ a)
symmetric {a} {b} ab Q = ab P (reflexive Q)
    P : A → Set
    P c = (Q c → Q a)

The symmetry is tricky, but not complicated. Shortly ab P has type (Q a → Q a) → (Q b → Q a).

I tried out few things on a paper using these rules. Things seem to work out rather well and it's really easy compared to identity type.

congruence : (a ≡ b) → (f a ≡ f b)
congruence ab Q = ab (Q ∘ f)

To prove congruence, you prepend function into the constructor.

pair-eq : (a ≡ b) → (c ≡ d) → ((a,c) ≡ (b,d))

To prove that pairs are equal, you first construct ((a,c) ≡ (b,c)), then construct ((b,c) ≡ (b,d)), then use transitivity.

sum-conflict : (inl a = inr b) → 0

To prove that items are not equal, you first prove that an element of type 1 is same as element of type 0, then you provide the constant. Helper function to do that:

P c = case c of inl a → 1; inr b → 0

This all is really motivating me to study dependent types because you only need dependent product for leibniz equality.

Similar posts