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).
  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)).
About these ads

About Nicolai Kraus

Student 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?

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s