`{P : A -> Type} {u v : sig P} (pq : { p : u.1 = v.1 & p # u.2 = v.2 }) : (path_sigma_uncurried _ _ _ pq)..2 = ap (fun s => transport P s u.2) (pr1_path_sigma_uncurried pq) @ pq.2. Proof. destruct u as [u1 u2]; destruct v as [v1 v2]; simpl in *. destruct pq as [p q]. destruct p; simpl in q; destruct q; reflexivity. Defined.
Require Import HoTT.Basics. Require Import Types.Arrow Types.Paths.