## A direct proof of Hedberg’s theorem

In his article published 1998, Michael Hedberg has shown that a type with decidable equality also features the uniqueness of identity proofs property. Reading through Nils Anders Danielsson’s Agda formalization, I noticed that the statement “A has decidable equality”, i.e. $\forall x, y : A . (x \leadsto y) + (x \leadsto y \rightarrow \bot)$, looks pretty similar to “A is contractible”, i.e. $\exists x : A . \forall y : A. x \leadsto y$. Therefore, it is not at all surprising that a slight modification of the proof that the h-level is upwards closed works as a more direct proof for Hedberg’s theorem than the original one, but I want to share my Coq-Code anyway.

There is also a simple slight improvement of the theorem, stating that “local decidability of equality” implies “local UIP”. I use the definition of the identity type and some basic properties from Andrej Bauer’s github.

A file containing the complete Coq code (inclusive the lines that are necessary to make the code below work) can be found here.

I first prove a (local) lemma, namely that any identity proof is equal to one that can be extracted from the decidability term dec. Of course, this is already nearly the complete proof. I do that as follows: given $x$ and $y \in A$ and a proof $p$ that they are equal, I check what $\mathtt{dec}$ “thinks” about $x$ and $y$ (as well as $x$ and $x$). If $\mathtt{dec}$ tells me they are not equal, I get an obvious contradiction. Otherwise, $\mathtt{dec}$ precisely says that they are in the same “contractible component”, so I can just go on as in the proof that the h-level is upwards closed. With this lemma at hand, the rest is immediate.

Theorem hedberg A : dec_equ A -> uip A.
Proof.
intros A dec x y.

assert (
lemma :
forall proof : x ~~> y,
match dec x x, dec x y with
| inl r, inl s => proof ~~> !r @ s
| _, _ => False
end
).
Proof.
induction proof.
destruct (dec x x) as [pr | f].
apply opposite_left_inverse.
exact (f (idpath x)).

intros p q.
assert (p_given_by_dec := lemma p).
assert (q_given_by_dec := lemma q).
destruct (dec x x).
destruct (dec x y).
apply (p_given_by_dec @ !q_given_by_dec).
Qed.

Christian Sattler has pointed out to me that the above proof can actually be used to show the following slightly stronger version of Hedberg’s theorem (again, see here), stating that “local decidability implies local UIP”:

Theorem hedberg_strong A (x : A) :
(forall y : A, decidable (x ~~> y)) ->
(forall y : A, proof_irrelevant (x ~~> y)).

At the University of Nottingham
This entry was posted in Code. Bookmark the permalink.

### 5 Responses to A direct proof of Hedberg’s theorem

1. Mike Shulman says:

Interesting! Is the proof in the HoTT repository equivalent to either Hedberg’s proof or yours?

• Mike Shulman says:

(That proof is written out in prose on the nLab page h-set.)

• Thanks for the links! I think the nlab proof uses indeed a similar approach. Sorry, I was not aware of that. But to be honest, I don’t understand it completely. It says

Let $r$ be the image of $(1_x,p) \in \textit{Paths}_{A \times A}((x,x),(x,x))$ under the section $d$.

Does this implicitly use that $f : A \rightarrow B$ gives rise to $\textit{Paths}_A \rightarrow \textit{Paths}_B$ ? Is $(1_x, p)$ viewed as a “subset” of $(A \times A) \times (A \times A)$ ?

I’ll need to have a closer look at the Coq code in the HoTT repository to understand how exactly it works.

• Mike Shulman says:

It means what the HoTT repository calls map_dep, which is a dependent version of $f\colon A\to B$ giving rise to $map(f)\colon Paths_A \to Paths_B$.