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