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

Question

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?

Answer 1

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.