Commit 2026-05-06 00:44 444855cc

refactor(CategoryTheory/Limits): redefine IsIPC in terms of IsIPCOfShape (#38378) A category C satisfies the w-IPC property if w-sized filtered colimits commute with w-sized products. We introduce an intermediate class IsIPCOfShape which says that w-sized filtered colimits commute with products of the given shape and redefine IsIPC in terms of it. We also rephrase the condition as a certain cocone being colimiting instead of some morphism being an isomorphism. This allows to remove some colimit existence assumptions. The motivation for this is to give a tighter condition for when ObjectProperty.ind is stable under products of a certain shape. From Proetale.