fact: 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.
imports: UniMath.Foundations.Preamble