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.





leanprover-community/mathlib,leanprover-community/mathlib