{A : Type} {B : A -> Type} {C : sig B -> Type} {x1 x2 : A} {p : x1 = x2} (y1 : { y : B x1 & C (x1; y) }) (y2 : { y : B x2 & C (x2; y) }) : {n : DPath B p y1.1 y2.1 & DPath C (path_sigma_dp (p; n)) y1.2 y2.2} <~> DPath (fun x => { y : B x & C (x; y) }) p y1 y2. Proof. destruct p. refine (path_sigma_dp oE _). apply equiv_functor_sigma_id. cbn; intro q. destruct y1 as [y11 y12], y2 as [y21 y22]. cbn in *. by destruct q. Defined.
Require Import Basics. Require Import Types.Paths Types.Sigma Types.Forall.