Definition transportf_total2 {A : UU} {B : A -> UU} {C : ∏ a:A, B a -> UU} {x1 x2 : A} (p : x1 = x2) (yz : ∑ y : B x1, C x1 y) : transportf (λ x, ∑ y : B x, C x y) p yz = tpair (λ y, C x2 y) (transportf _ p (pr1 yz)) (transportD _ _ p (pr1 yz) (pr2 yz)). Proof. intros. induction p. induction yz. apply idpath. Defined.