# Does equality in $\Sigma_{(x : X)} x = x$ implies UIP?

The short version:

Is this statement correct? If it is, is it provable in Coq?

Definition id_at { X : Set } ( x : X ) := x = x.
Definition id_at_eq_refl { X : Set } { x : X } ( p : x = x ) := existT id_at x p = existT id_at x eq_refl.
Proposition id_at_eq_refl_uip { X : Set } { x : X }
: (forall (p : x = x), id_at_eq_refl p)
-> (forall (p : x = x), p = eq_refl).


I recently stumbled upon the post Dependent Pair Injectivity equivalent to K on Coq Discourse. The key idea to proof $$DPI \implies K$$ is that for a fixed (x : X) and any proof (p : x = x), existT (fun y => y = x) x p = existT (fun y => y = x) x eq_refl always holds.

However, if we change the (fun y => y = x) to (fun y => y = y), this equality does not hold. Later I found out that this is discussed in the HoTT book (Remark 1.12.1), and my understanding is that this is due to both end of the equality being fixed. This distinguishes the based loop space from the free path space, and in the based loop space one cannot just unwind the equality p and stay inside the space.

Another (maybe incorrect) observation of mine is that in the context of HoTT, if we choose $$X = S^1$$, moving around inside the based loop space $$\Sigma_{(x : S^1)} x = x$$ is same as changing the base point of the loop, and does not change the winding number of $$p$$. So $$(x, p) = (x, \mathsf{refl})$$ forces $$p = \mathsf{refl}$$.

So the question is can this generalize to other types, in contexts other than HoTT: For a given type $$X$$, Assuming for all proof $$p : x = x$$, the pair $$(x, p)$$ is equal to $$(x, \mathsf{refl}_x)$$ in the type $$\Sigma_{(x : X) x = x}$$, can we claim that x have unique identity proof, that is, $$\forall (p : x = x), p = \mathsf{refl}_x$$, even without the injectivity of dependent pairs?

• HoTT book page numbers are unsable, please refer to the suitable section/lemma/theorem. Commented Jan 25 at 10:59
• @andrej-bauer Sorry. I've updated the question to use the numbered remark. Commented Jan 25 at 11:11
• By the way id_at is known as the loop space at $x$. Also, have you tried to prove the statement? Where did you get stuck? Commented Jan 25 at 12:08
• @andrej-bauer I was mostly just trying to get an intuition of the correctness of the statement (in the settings of HoTT). I thought it would needs that $\Omega X$ splits, but later found out that the statement was precisely "if the loop space is path-connected, then the base space is simply connected", which should be true. Commented Jan 26 at 10:51

Indeed, it holds:

Definition id_at { X : Set } ( x : X ) := x = x.
Definition id_at_eq_refl { X : Set } { x : X } ( p : x = x ) := existT id_at x p = existT id_at x eq_refl.
Proposition id_at_eq_refl_uip { X : Set } { x : X }
: (forall (p : x = x), id_at_eq_refl p)
-> (forall (p : x = x), p = eq_refl).
Proof.
intros H p.
specialize (H p). unfold id_at_eq_refl in H.
assert (projT2 (existT id_at x eq_refl) = @eq_refl _ (projT1 (existT id_at x eq_refl))) as Heqr by reflexivity.
revert H Heqr.
generalize (existT id_at x eq_refl) as k.
intros k. intros <-. simpl. easy.
Qed.


The reason it works is interesting. We can generalize existT id_at x eq_refl as k, but still remember that its second component was eq_refl, because the type of projT2 k and eq_refl (on projT1 k) are the same (namely, id_at). Therefore, the first equality becomes usable (using an equality here usually means that you have to have the right-hand side be an unconstrained variable), so we can replace an eq_refl by p but still remember that it was eq_refl before, giving us p = eq_refl.

• Can we use H to rewrite Heqr and avoid the generalize step? This is actually really interesting. Previously I tried to just use f_equal (or just prove that applying projT2 to both end of the equality still yields a equality, then use simpl), but projT2 is dependent, and the dependent version f_equal_dep doesn't not directly yield the required equality. That is what actually where the DPI comes into play in the DPI => K proof. Commented Jan 26 at 11:22
• @LiuXiaoyi You can likely make the proof shorter. The one I originally found was, I made it longer to make it more didactic, and would be happy to see a more compact version. Commented Jan 27 at 9:54
• @LiuXiaoyi also note that you can not avoid the generalize step, since that is required by how matches on eq necessarily work. You can merely make it implicit, i.e. have rewrite infer the right abstraction automatically by massaging the goal. You might be able to cleverly construct a proof term using f_equal and some tricky conversions. Commented Feb 1 at 23:35