∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} (α : F ⟶ G) {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  α.naturality (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.Bicategory.whiskerRightIso (F.mapComp f g) (α.app c) ≪≫
      CategoryTheory.Bicategory.associator (F.map f) (F.map g) (α.app c) ≪≫
        CategoryTheory.Bicategory.whiskerLeftIso (F.map f) (α.naturality g) ≪≫
          (CategoryTheory.Bicategory.associator (F.map f) (α.app b) (G.map g)).symm ≪≫
            CategoryTheory.Bicategory.whiskerRightIso (α.naturality f) (G.map g) ≪≫
              CategoryTheory.Bicategory.associator (α.app a) (G.map f) (G.map g) ≪≫
                CategoryTheory.Bicategory.whiskerLeftIso (α.app a) (G.mapComp f g).symm