∀ {C : Type u_1} {D : Type u_4} [inst : CategoryTheory.Category.{u_2, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_3, u_4} D] (F : CategoryTheory.Functor C D)
  {b₀ b₁ b₂ b₃ : CategoryTheory.LocallyDiscrete C} (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).toLoc)
            h))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.associator
              ((fun {b b'} x =>
                  match x with
                  | { as := f } => (F.map f).toLoc)
                f)
              ((fun {b b'} x =>
                  match x with
                  | { as := f } => (F.map f).toLoc)
                g)
              ((fun {b b'} x =>
                  match x with
                  | { as := f } => (F.map f).toLoc)
                h)).hom
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Bicategory.whiskerLeft
              ((fun {b b'} x =>
                  match x with
                  | { as := f } => (F.map f).toLoc)
                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 ⋯