Definition transportf_id3 {A : UU} {x1 x2 : A} (p : x1 = x2) (q : x1 = x1) : transportf (λ (x : A), x = x) p q = !p @ q @ p. Proof. intros. induction p. simpl. apply pathsinv0. apply pathscomp0rid. Defined.