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 hSets, 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 Hs 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.
