proposition: Lemma transport_pr1_path_sigma_uncurried `{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: Proof. destruct pq as [p q], u, v; simpl in *. destruct p, q; simpl in *. reflexivity. Defined.
imports: HoTT.Basics Types.Arrow Types.Paths