∀ (B : Type u_1) [inst : CategoryTheory.Bicategory B] (C : Type u_2) [inst_1 : CategoryTheory.Bicategory C]
  {a b : B × C} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h),
  (CategoryTheory.CategoryStruct.comp η θ).2 = CategoryTheory.CategoryStruct.comp η.2 θ.2