{A P} {x x' : A} {y : P x} {y' : P x'} : {p : x = x' & DPath P p y y'} <~> (x; y) = (x'; y') := equiv_path_sigma P (x; y) (x'; y').
Require Import Basics. Require Import Types.Paths Types.Sigma Types.Forall.