{𝒮 : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} 𝒮} →
    {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} →
      {X Y : F.Grothendieck} → X.Hom Y → ℕ