Definition transport_section {X : UU} {P:X -> UU} (f : ∏ x, P x) {x : X} {y : X} (e : x = y) : transportf P e (f x) = f y. Proof. intros. exact (transport_map (P:= λ _,unit) (λ x _,f x) e tt). Defined.