mathlib

6b35819b - refactor(category_theory): make `has_image` and friends a Prop (#4195)

refactor(category_theory): make `has_image` and friends a Prop (#4195) This is an obious follow-up to #3995. It changes the following declarations to a `Prop`: * `arrow.has_lift` * `strong_epi` * `has_image`/`has_images` * `has_strong_epi_mono_factorisations` * `has_image_map`/`has_image_maps` The big win is that there is now precisely one notion of exactness in every category with kernels and images, not a (different but provably equal) notion of exactness per `has_kernels` and `has_images` instance like in the pre-#3995 era.