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