feat(category_theory): regular monos (#2154)
* feat(category_theory): regular and normal monos
* fixes
* Apply suggestions from code review
Co-Authored-By: Markus Himmel <markus@himmel-villmar.de>
* shorter proofs
* typos, thanks
Co-Authored-By: Markus Himmel <markus@himmel-villmar.de>
* Update src/category_theory/limits/shapes/regular_mono.lean
Co-Authored-By: Markus Himmel <markus@himmel-villmar.de>
* linting
Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
