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