{P : Sort u_1} →
  {C : Type u₁} →
    {inst : CategoryTheory.Category.{v₁, u₁} C} →
      {J : CategoryTheory.GrothendieckTopology C} →
        {R : CategoryTheory.Sheaf J RingCat} →
          {t : SheafOfModules R} →
            {C' : Type u₁} →
              {inst' : CategoryTheory.Category.{v₁, u₁} C'} →
                {J' : CategoryTheory.GrothendieckTopology C'} →
                  {R' : CategoryTheory.Sheaf J' RingCat} →
                    {t' : SheafOfModules R'} →
                      C = C' → inst ≍ inst' → J ≍ J' → R ≍ R' → t ≍ t' → SheafOfModules.noConfusionType P t t'