transport_sigma' {A B : Type} {C : A -> B -> Type} {x1 x2 : A} (p : x1 = x2) (yz : { y : B & C x1 y }) : transport (fun x => { y : B & C x y }) p yz = (yz.1 ; transport (fun x => C x yz.1) p yz.2). Proof. destruct p. destruct yz. reflexivity. Defined.
Require Import HoTT.Basics. Require Import Types.Arrow Types.Paths.