mathlib3

feat(category_theory): regular monos

#2154

Merged