∀ {B : Type u_2} [inst : CategoryTheory.Bicategory B] {F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat}
  (P : F.ObjectProperty) [inst_1 : P.IsClosedUnderMapObj] {a b c : B} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c),
  { toNatTrans := P.map₂ (CategoryTheory.Bicategory.whiskerRight η h) } =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Cat.Hom.isoMk (P.mapComp f h)).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight { toNatTrans := P.map₂ η } { toFunctor := P.map h })
        (CategoryTheory.Cat.Hom.isoMk (P.mapComp g h)).inv)