Definition weq_transportf_adjointness {X Y : UU} (w : X ≃ Y) (P : Y -> UU) (x : X) (p : P (w x)) : transportf (P ∘ w) (! homotinvweqweq w x) p = transportf P (! homotweqinvweq w (w x)) p. Proof. intros. refine (functtransportf w P (!homotinvweqweq w x) p @ _). apply (maponpaths (λ e, transportf P e p)). rewrite maponpathsinv0. apply maponpaths. apply homotweqinvweqweq. Defined.