Uniqueness of Identity Proof from Decidable Equality, the Easy Way
For some reason, there always comes a time every other year when I’m around a table that discusses the reason that decidable equality implies uniqueness of identity proofs. In most cases, the people present converge to stating that the equality given by the decidability proof is the center of contraction, and that it should be easy to continuously deform every other equality to it. At some point, someone becomes bored of the subject and throws an “anyway, this is Hedberg’s theorem, right?” concluding our interesting yet unfruitful musings.
However, I always felt that Hedberg’s theorem was lacking meaning for me: defining a binary mere reflexive relation that implies identity, then showing its equivalence to the identity seems like a roundabout way to go about things.
But recently, I’ve stumbled upon a beautiful proof in Rocq’s standard library that satisfies all the sore points in ways Hedberg’s theorem does not. So, let’s open this small formalization right away.
Section DecEq.
This proof is quite straightforward, and perfectly formalizes the arguments that (i) the equality given by the decidability proof is the center of contraction, and (ii) every other equality easily continuously deform to it. Let us assume a type $A$ and decidable equality on this type throughout this section, i.e., in Rocq code:
Context {A : Type} (deceq : forall {x y : A}, { x = y } + { x <> y }).
The trick of the proof is in defining the following constant function, that always sends an equality to the “center of contraction”, i.e., the equality given by the decidability hypothesis.
Definition g {x y : A} (p : x = y) : x = y :=
match deceq x y with
| left e => e
| right n => False_ind (x = y) (n p)
end.
Then, one can show that every path $p : x = y$ can be continuously deformed to $(g~ \textsf{refl})^{-1} \cdot g~p$: proceeding by induction on $p$, it suffices to give a path between $(g~\textsf{refl})^{-1} \cdot g~\textsf{refl}$, which is easy.
Lemma rew_eq : forall {x y : A} (p : x = y), p = eq_trans (eq_sym (g (@eq_refl _ x))) (g p).
Proof using Type.
intros; destruct p. symmetry.
apply eq_trans_sym_inv_l.
Qed.
In turn, it means that for every $p, q : x = y$, we have to show that:
$(g~\textsf{refl})^{-1} \cdot (g~p) = (g~\textsf{refl})^{-1} \cdot (g~q)$,
which is obviously true as both $g~p$ and $g~q$ are the center of contraction.
Theorem UIP : forall {x y : A} {p q : x = y}, p = q.
Proof using deceq.
intros; rewrite (rew_eq p), (rew_eq q).
unfold g; now destruct (deceq x y).
Qed.
And voilà, we now have a beautiful 6-lines formalized proof of uniqueness of identity proofs from decidability of equality. That was easy, right?
End DecEq.