From c3174fe29b5f0a9ca4d0ce4d6351ace25d3a5a6e Mon Sep 17 00:00:00 2001
From: Dan Frumin <dan@groupoid.moe>
Date: Mon, 14 Jun 2021 15:58:10 +0200
Subject: [PATCH] add a missing blogpost

---
 content/leibniz-equality.md | 83 +++++++++++++++++++++++++++++++++++++
 1 file changed, 83 insertions(+)
 create mode 100644 content/leibniz-equality.md

diff --git a/content/leibniz-equality.md b/content/leibniz-equality.md
new file mode 100644
index 0000000..4ad1fe0
--- /dev/null
+++ b/content/leibniz-equality.md
@@ -0,0 +1,83 @@
+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.