mathlib3

e6aa533b - fix(category_theory/limits): remove an unnecessary axiom in has_image_map (#2455)

fix(category_theory/limits): remove an unnecessary axiom in has_image_map (#2455) I somehow missed the fact that `has_image_map.factor_map` is actually a consequence of `has_image_map.map_ι` together with the fact that `image.ι` is always a monomorphism.