Lemma two_arg_paths_f {A : UU} {B : A -> UU} {C:UU} {f : ∏ a, B a -> C} {a1 b1 a2 b2} (p : a1 = a2) (q : transportf B p b1 = b2) : f a1 b1 = f a2 b2. Proof. intros. induction p. induction q. apply idpath. Defined.