Ever since I learned Coq I was fascinated by the equivalence between dependent pair injectivity (DPI) and K. There are long winded proofs in the Coq library EqdepFacts. It turns out there are very short proofs for both direction. The trick for the direction K to DPI was given to me by Gaëtan Gilbert on Friday at Coq Club, and this was a real eye opener. Below are short proofs for both directions. Each direction has a lemma expressing a clever generalization making the proof go through. Code is below. Please tell me if the proofs have been posted before. Gert

```
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.
intros H [] e. destruct (H _ e). reflexivity.
Qed.
Fact K_DPI X p :
K X -> DPI X p.
Proof.
intros 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.
intros []. reflexivity.
Qed.
Fact DPI_K X :
(forall p, DPI X p) -> K X.
Proof.
intros H x e. apply (H (fun z => z = x)), DPI_K'.
Qed.
```