Definition transport_b_f {X : UU} (P : X ->UU) {x y z : X} (e : x = y) (e' : z = y) (p : P x) : transportb P e' (transportf P e p) = transportf P (e @ !e') p. Proof. intros. induction e'. induction e. apply idpath. Defined.