Commit 2020-03-16 23:16 4754368c

feat(category_theory): split epis and monos, and a result about (co)projections (#2146)

• feat(category_theory): split epis and monos, and a result about (co)projections
• rearranging
• reviewers' suggestions
• A split mono f equalizes (retraction f ≫ f) and (𝟙 Y).
• fix
• cleanup
• split_epi_coequalizes
• fix
• cleanup
• reduce priorities
• Update src/category_theory/epi_mono.lean Co-Authored-By: Yury G. Kudryashov urkud@urkud.name
• Update src/category_theory/epi_mono.lean