{P : Sort u} →
  {𝒮 : Type u₁} →
    {inst : CategoryTheory.Category.{v₁, u₁} 𝒮} →
      {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} →
        {X Y : F.Grothendieck} →
          {t : X.Hom Y} →
            {𝒮' : Type u₁} →
              {inst' : CategoryTheory.Category.{v₁, u₁} 𝒮'} →
                {F' : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮') CategoryTheory.Cat} →
                  {X' Y' : F'.Grothendieck} →
                    {t' : X'.Hom Y'} →
                      𝒮 = 𝒮' →
                        inst ≍ inst' →
                          F ≍ F' →
                            X ≍ X' →
                              Y ≍ Y' → t ≍ t' → CategoryTheory.Pseudofunctor.Grothendieck.Hom.noConfusionType P t t'