∀ {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₁ : CategoryTheory.LocallyDiscrete C} (f : b₀ ⟶ b₁),
  CategoryTheory.CategoryStruct.comp
      ((fun {b₀ b₁ b₂} f g => CategoryTheory.eqToIso ⋯) (CategoryTheory.CategoryStruct.id b₀) f).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight
          ((fun x =>
                match x with
                | { as := X } => CategoryTheory.eqToIso ⋯)
              b₀).hom
          ((fun {b b'} x =>
              match x with
              | { as := f } => (F.map f).toLoc)
            f))
        (CategoryTheory.Bicategory.leftUnitor
            ((fun {b b'} x =>
                match x with
                | { as := f } => (F.map f).toLoc)
              f)).hom) =
    CategoryTheory.eqToHom ⋯