mathlib

583a7034 - feat(category_theory): a characterization of separating objects (#14838)