path_sigma' {A : Type} (P : A -> Type) {x x' : A} {y : P x} {y' : P x'} (p : x = x') (q : p # y = y') : (x;y) = (x';y') := path_sigma P (x;y) (x';y') p q.
Require Import HoTT.Basics. Require Import Types.Arrow Types.Paths.