∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} {f : a ⟶ b} {g : b ⟶ c} {h i : c ⟶ d} {η : h ⟶ i}
  {η₁ : CategoryTheory.CategoryStruct.comp g h ⟶ CategoryTheory.CategoryStruct.comp g i}
  {η₂ :
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h) ⟶
      CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g i)}
  {η₃ :
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h) ⟶
      CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) i}
  {η₄ :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h ⟶
      CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) i},
  CategoryTheory.Bicategory.whiskerLeft g η = η₁ →
    CategoryTheory.Bicategory.whiskerLeft f η₁ = η₂ →
      CategoryTheory.CategoryStruct.comp η₂ (CategoryTheory.Bicategory.associator f g i).inv = η₃ →
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).hom η₃ = η₄ →
          CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.comp f g) η = η₄