Leibniz equality states that two things are equal if they are
industinguishable by any predicates. For a type `A`

and `a, b : A`

:

```
Leq(A, a, b) ≡ ∏ (P : A → Prop), P a ⇔ P b
```

In the language of HoTT we can restate the definition slightly:

```
Leq(A, a, b) ≡ ∏ (P : A → hProp), P a = P b
```

where the last equality is equality of hProps: `P a =_hProp P b`

.
Since `hProp : hSet`

, we have that `P a =_hProp P b : hProp`

and,
hence `Leq(A, a, b) : hProp`

.

Because `Leq`

is a proposition it cannot describe fully the actual
identity type `Id(A, a, b)`

. But it does accurately desctibe the
equality in hSets.

Let `A : hSet`

. Then we can define `Leq(A, a, b) <-> Id(A, a, b)`

.
First, we define `f : Id(A, a, b) → Leq(A, a, b)`

by

```
f(p : a = b) ≡ λ (P : A → hProp). ap P p
```

In the other direction we define `g : Leq(A, a, b) → Id(A, a, b)`

.
Suppose we have `H : Leq(A, a, b)`

. Then we just pick `h(x) ≡ (a = x)`

,
and `H(h) : (a = a) = (a = b)`

, which we apply to `1_a`

.

```
g(H : ∏ P, P a = P b) ≡
let h = (λx. a = x) : A → hProp in
transport (λ X. X) (H(h)) (idpath a)
```

So, for the equality on `hSet`

s, the Leibniz equality coincides with
the ML indentity type.

The question that I have is whether we can generalize it and define a complete tower of Leibniz equalities? This is what I mean, specifically.

For an (n+1)-Type `A`

and `a, b : A`

, we can define `Leq_n(A, a, b) : n-Type`

as:

```
Leq_n(A, a, b) ≡ ∏ (P : A → n-Type), P a =_{n-Type} P b
```

We can still reuse the same functions `f`

and `g`

, which type check
correctly. We can also show:

```
g(f(p : a = b)) = p
```

By induction

```
g(f(1_a)) = g(λP. ap P 1_a) = g (λP. 1_{P_a}) =
(idpath (h(a) = h(a)))*(1_a) = 1_a
```

So we have a section `a = b → Leq_n(A, a, b)`

. But showing that `f(g(H)) = H`

is complicated. It would be nice to see if it can be derived
somehow.

In order to show that `f(g(H)) = H`

, you need to show that for any `P`

,

```
ap P (transport (H (λx. a = x)) 1a) = H P
```

Note that all the elements in the image of `f`

satisfy this condition.
So perhaps it will make sense to restrict the type `Leq(A, a, b)`

to
contain only such `H`

s that satisfy the condition above?
I am not sure, but it is something that might be worth looking into.

Note that the definition of Leibniz equality that we consider here is different from the "unrestricted" Leibniz equality:

```
Leq_Type(A, a, b) ≡ ∏ (P : A → Type), P a ↔ P b
```

This Leibniz equality type has been studied in the context of intensional type theory in "Leibniz equality is isomorphic to Martin-Löf identity, parametrically" by Abel, Cockx, Devriese, Timany, and Wadler.
They show that, under the assumptions of parametricity/under the parametricity translation, the above `Leq_Type`

is isomorphic to the standard intensional equality type.

It might be interesting to compare the "truncated" and "unrestricted" Leibniz equality types.
For example, we can represent a type as a colimit of a sequence of n-truncations.
Does this connection somehow lift to representation of `Leq_Type`

in terms of `Leq_n`

's?

Let me know if you have any ideas on this topic.