{P : Sort u_1} →
  {P_1 : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
    {S : AlgebraicGeometry.Scheme} →
      {t : AlgebraicGeometry.Scheme.AffineCover P_1 S} →
        {P' : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
          {S' : AlgebraicGeometry.Scheme} →
            {t' : AlgebraicGeometry.Scheme.AffineCover P' S'} →
              P_1 = P' → S = S' → t ≍ t' → AlgebraicGeometry.Scheme.AffineCover.noConfusionType P t t'