mathlib

3b195032 - refactor(category_theory/single_obj): migrate to bundled morphisms (#1330)

refactor(category_theory/single_obj): migrate to bundled morphisms (#1330) * Define equivalence between `{ f // is_monoid_hom f }` and `monoid_hom` * Migrate `single_obj` to bundled homomorphisms Fix a bug in `to_End`: the old implementation used a wrong monoid structure on `End`. * Fix `Mon.hom_equiv_monoid_hom` as suggested by @jcommelin