`{P : A -> Type} {u v : sig P} (p : u.1 = v.1) (q : p # u.2 = v.2) Q : transport (fun x => Q x.1) (@path_sigma A P u v p q) = transport _ p := transport_pr1_path_sigma_uncurried (p; q) Q. Global Instance isequiv_path_sigma `{P : A -> Type} {u v : sig P} : IsEquiv (path_sigma_uncurried P u v) | 0. Proof. simple refine (Build_IsEquiv _ _ _ (fun r => (r..1; r..2)) eta_path_sigma _ _). all: destruct u, v; intros [p q]. all: simpl in *. all: destruct q, p; simpl in *. all: reflexivity. Defined.
Require Import HoTT.Basics. Require Import Types.Arrow Types.Paths.