Lemma total2_paths2_f {A : UU} {B : A -> UU} {a1 : A} {b1 : B a1} {a2 : A} {b2 : B a2} (p : a1 = a2) (q : transportf B p b1 = b2) : a1,,b1 = a2,,b2. Proof. intros. exact (two_arg_paths_f p q). Defined.