Definition weq_transportb_adjointness {X Y : UU} (w : X ≃ Y) (P : Y -> UU) (x : X) (p : P (w x)) : transportb (P ∘ w) (homotinvweqweq w x) p = transportb P (homotweqinvweq w (w x)) p. Proof. intros. refine (functtransportb w P (homotinvweqweq w x) p @ _). apply (maponpaths (λ e, transportb P e p)). apply homotweqinvweqweq. Defined.