Commit 2020-04-19 15:18 e6aa533b

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.