Leibniz equality for truncated types in HoTT


Tags: type theory

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.