∀ {B₀ : Type u_4} {C : Type u_2} [inst : CategoryTheory.Category.{u_5, u_4} B₀] [inst_1 : CategoryTheory.Bicategory C]
  (obj : B₀ → C) (map : {b b' : B₀} → (b ⟶ b') → (obj b ⟶ obj b')) {b₀ b₁ b₂ b₃ : CategoryTheory.LocallyDiscrete B₀}
  (x : b₀ ⟶ b₁) (x_1 : b₁ ⟶ b₂) (x_2 : b₂ ⟶ b₃),
  map (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp x.as x_1.as) x_2.as) =
    map (CategoryTheory.CategoryStruct.comp x.as (CategoryTheory.CategoryStruct.comp x_1.as x_2.as))