{A : Type} (P : A -> Type) {u v w : sig P} (p1 : u.1 = v.1) (q1 : p1 # u.2 = v.2) (p2 : v.1 = w.1) (q2 : p2 # v.2 = w.2) : path_sigma P u w (p1 @ p2) (transport_pp P p1 p2 u.2 @ ap (transport P p2) q1 @ q2) = path_sigma P u v p1 q1 @ path_sigma P v w p2 q2. Proof. destruct u, v, w. simpl in *. destruct p1, p2, q1, q2. reflexivity. Defined.
Require Import HoTT.Basics. Require Import Types.Arrow Types.Paths.