Saturated reflection from a strong-subobject intersection (source code)

= Saturated reflection from a strong-subobject intersection

Suppose a complete well-powered category has enough objects saturated with respect to anodyne morphisms. Inside a saturated object containing $A$, intersect all strong subobjects containing $A$. The resulting object is saturated, the map from $A$ to it is anodyne, and its extension property makes it the reflection of $A$ into the full subcategory of saturated objects.