path_sigma_p1_1p' {A : Type} (P : A -> Type) {u1 v1 : A} {u2 : P u1} {v2 : P v1} (p : u1 = v1) (q : p # u2 = v2) : path_sigma' P p q = path_sigma' P p 1 @ path_sigma' P 1 q. Proof. destruct p, q. reflexivity. Defined.
Require Import HoTT.Basics. Require Import Types.Arrow Types.Paths.