Definition transportf_dirprod (A : UU) (B B' : A -> UU) (x x' : ∑ a, B a × B' a) (p : pr1 x = pr1 x') : transportf (λ a, B a × B' a) p (pr2 x) = make_dirprod (transportf (λ a, B a) p (pr1 (pr2 x))) (transportf (λ a, B' a) p (pr2 (pr2 x))). Proof. induction p. apply idpath. Defined.