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