{A : Type} {B : A -> Type} {C : forall a:A, B a -> Type} {x1 x2 : A} (p : x1 = x2) (yz : { y : B x1 & C x1 y }) : transport (fun x => { y : B x & C x y }) p yz = (p # yz.1 ; transportD _ _ p yz.1 yz.2). Proof. destruct p. destruct yz as [y z]. reflexivity. Defined.
Require Import HoTT.Basics. Require Import Types.Arrow Types.Paths.