{P : Sort u} →
  {𝒮 : Type u₁} →
    {inst : CategoryTheory.Category.{v₁, u₁} 𝒮} →
      {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} →
        {t : F.CoGrothendieck} →
          {𝒮' : Type u₁} →
            {inst' : CategoryTheory.Category.{v₁, u₁} 𝒮'} →
              {F' : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮'ᵒᵖ) CategoryTheory.Cat} →
                {t' : F'.CoGrothendieck} →
                  𝒮 = 𝒮' →
                    inst ≍ inst' → F ≍ F' → t ≍ t' → CategoryTheory.Pseudofunctor.CoGrothendieck.noConfusionType P t t'