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. , looks pretty similar to “A is contractible”, i.e. . 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 and and a proof that they are equal, I check what “thinks” about and (as well as and ). If tells me they are not equal, I get an obvious contradiction. Otherwise, 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). contradiction. contradiction. 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)).
Interesting! Is the proof in the HoTT repository equivalent to either Hedberg’s proof or yours?
(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 be the image of under the section .
Does this implicitly use that gives rise to ? Is viewed as a “subset” of ?
I’ll need to have a closer look at the Coq code in the HoTT repository to understand how exactly it works.
It means what the HoTT repository calls map_dep, which is a dependent version of giving rise to .
Now I got it, thanks!