Sort u_1 →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {ι : Type w} →
        {I : CategoryTheory.Limits.MultispanIndex (CategoryTheory.Limits.MultispanShape.prod ι) C} →
          I.SymmStruct →
            {C' : Type u} →
              [inst' : CategoryTheory.Category.{v, u} C'] →
                {ι' : Type w} →
                  {I' : CategoryTheory.Limits.MultispanIndex (CategoryTheory.Limits.MultispanShape.prod ι') C'} →
                    I'.SymmStruct → Sort u_1