# 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)`

`where`

`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.