∀ {I : Type u_1} {B : Type u_5} [inst : CategoryTheory.Category.{u_2, u_1} I] [inst_1 : CategoryTheory.Bicategory B]
  [inst_2 : CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B)
  {b₀ b₁ b₂ b₃ : CategoryTheory.LocallyDiscrete I} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃),
  CategoryTheory.CategoryStruct.comp
      ((fun {b₀ b₁ b₂} f g => CategoryTheory.eqToIso ⋯) (CategoryTheory.CategoryStruct.comp f g) h).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight ((fun {b₀ b₁ b₂} f g => CategoryTheory.eqToIso ⋯) f g).hom
          ((fun {b b'} x =>
              match x with
              | { as := f } => F.map f)
            h))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.associator
              ((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)
              ((fun {b b'} x =>
                  match x with
                  | { as := f } => F.map f)
                h)).hom
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Bicategory.whiskerLeft
              ((fun {b b'} x =>
                  match x with
                  | { as := f } => F.map f)
                f)
              ((fun {b₀ b₁ b₂} f g => CategoryTheory.eqToIso ⋯) g h).inv)
            ((fun {b₀ b₁ b₂} f g => CategoryTheory.eqToIso ⋯) f (CategoryTheory.CategoryStruct.comp g h)).inv))) =
    CategoryTheory.eqToHom ⋯