Commit 2025-10-29 00:03 ce4bea0e

feat(CategoryTheory): strong generators (#29519) In this PR, we introduce a condition IsStrongGenerator P on P : ObjectProperty C which is stronger than IsSeparating P as we also require that for any proper subobject A ⊂ X, there exists a morphism G ⟶ X from an object satisfying P which does not factor through A. In case coproducts exists, we give a characterization of IsStrongSeparator P in terms of the existence, for each object X : C of an extremal epi to X from a coproduct of objects in S. In future works (#30241), this shall be used in order to characterize locally κ-presentable categories as cocomplete categories that have a strong generator consisting of κ-presentable objects.