Commit 2025-02-21 15:59 7fd6bf1d

feat(CategoryTheory/Limits/Fubini): relax HasLimits hypotheses (#20570) Add a proof that one can construct a limit cone for a functor (G : J × K ⥤ C) out of a limit cone for curry.obj G ⋙ lim (provided the latter makes sense). From this deduce that C has limits of shape J × K if it has limits of shape J and of shape K. Remove the now unnecessary assumptions in the Fubini theorem for limits. All statements have their colimit counterpart.