title: Leibniz equality for truncated types in HoTT
tags: type theory
date: 2021-01-19 00:00
---

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"](https://www.cambridge.org/core/journals/journal-of-functional-programming/article/abs/leibniz-equality-is-isomorphic-to-martinlof-identity-parametrically/50D76A9C314AB24E7CD46DA4A0A766EB) 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](https://homotopytypetheory.org/2014/06/30/fibrations-with-em-fiber/).
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.