Many algebraic structures in Lean initially used unbundled homs (e.g. a bare function between types, along with an is_monoid_hom typeclass), but the general trend is towards using bundled homs.
This file provides a basic infrastructure to define concrete categories using bundled homs, and define forgetful functors between them.
Class for bundled homs. Note that the arguments order follows that of lemmas for monoid_hom. This way we can use ⟨@monoid_hom.to_fun, @monoid_hom.id ...⟩ in an instance.
Every @bundled_hom c _ defines a category with objects in bundled c.
A category given by bundled_hom is a concrete category.
A version of has_forget₂.mk' for categories defined using @bundled_hom.