Commit 2020-09-24 02:35 6b35819b

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.