sigma injectivity ~= axiom K

DpiK.v

(* https://coq.discourse.group/t/dependent-pair-injectivity-equivalent-to-k/1112 *)
(* ported to SSReflect *)

From Coq Require Import ssreflect.

Notation Sig := existT.
Notation pi1 := projT1.
Notation pi2 := projT2.

Definition K X := forall (x : X) (e: x = x), eq_refl = e.
Definition DPI X (p: X -> Type) := forall x u v, Sig p x u = Sig p x v -> u = v.

Definition cast {X} {x y: X} {p: X -> Type}
  :  x = y -> p x -> p y
  := fun e a => match e with eq_refl => a end.

Lemma K_DPI' {X} {p: X -> Type} {a b: sigT p} :
  K X  -> a = b -> forall e: pi1 a = pi1 b, cast e (pi2 a) = pi2 b.
Proof. 
by move=>H -> e; rewrite -(H _ e).
Qed.

Fact K_DPI X p :
  K X -> DPI X p.
Proof.
by move=>H x u v e; apply/(K_DPI' H e eq_refl).
Qed.

Lemma DPI_K' X (x y: X) :
  forall e: x = y,
    Sig (fun z => z = y) y eq_refl = Sig (fun z => z = y) x e.
Proof.
by case: y /.
Qed.

Fact DPI_K X :
  (forall x, DPI X (fun z => z = x)) -> K X.
Proof.
by move=>H x e; apply/H/DPI_K'.
Qed.