Lemma transportf_fiber_total2_paths {A : UU} (B : A -> UU) (x y : ∑ x, B x) (p : pr1 x = pr1 y) (q : transportf _ p (pr2 x) = pr2 y) : transportf (λ p' : pr1 x = pr1 y, transportf _ p' (pr2 x) = pr2 y) (base_total2_paths q) (fiber_paths (total2_paths_f _ q)) = q. Proof. induction x as [x H]. induction y as [y K]. simpl in *. induction p. induction q. apply idpath. Defined.