∀ {I : Type u_4} {B : Type u_2} [inst : CategoryTheory.Category.{u_5, u_4} I] [inst_1 : CategoryTheory.Bicategory B]
  [inst_2 : CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B)
  {b₀ b₁ b₂ : CategoryTheory.LocallyDiscrete I} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂),
  (fun {b b'} x =>
        match x with
        | { as := f } => F.map f)
      (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp
      ((fun {b b'} x =>
          match x with
          | { as := f } => F.map f)
        f)
      ((fun {b b'} x =>
          match x with
          | { as := f } => F.map f)
        g)