This file provides basic infrastructure to define concrete categories using unbundled homs (see class unbundled_hom), and define forgetful functors between them (see unbundled_hom.mk_has_forget₂).
A class for unbundled homs used to define a category. hom must take two types α, β and instances of the corresponding structures, and return a predicate on α → β.
A custom constructor for forgetful functor between concrete categories defined using unbundled_hom.