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