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