Definition transport_map {X : UU} {P Q : X -> UU} (f : ∏ x, P x -> Q x) {x : X} {y : X} (e : x = y) (p : P x) : transportf Q e (f x p) = f y (transportf P e p). Proof. intros. induction e. apply idpath. Defined.