∀ {I : Type u_1} {B : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} I] [inst_1 : CategoryTheory.Bicategory B]
  [inst_2 : CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B)
  {X Y : CategoryTheory.LocallyDiscrete I} (x : X ⟶ Y), F.toPseudoFunctor'.map x = F.map x.as