A concrete category is a category C with a fixed faithful functor forget : C ⥤ Type*. We define concrete categories using class concrete_category. In particular, we impose no restrictions on the carrier type C, so Type is a concrete category with the identity forgetful functor.
Each concrete category C comes with a canonical faithful functor forget C : C ⥤ Type*. We say that a concrete category C admits a forgetful functor to a concrete category D, if it has a functor forget₂ C D : C ⥤ D such that (forget₂ C D) ⋙ (forget D) = forget C, see class has_forget₂. Due to faithful.div_comp, it suffices to verify that forget₂.obj and forget₂.map agree with the equality above; then forget₂ will satisfy the functor laws automatically, see has_forget₂.mk'.
Two classes helping construct concrete categories in the two most common cases are provided in the files bundled_hom and unbundled_hom, see their documentation for details.
See [Ahrens and Lumsdaine, Displayed Categories][ahrens2017] for related work.
A concrete category is a category C with a fixed faithful functor forget : C ⥤ Type.
The forgetful functor from a concrete category to Type u.
Provide a coercion to Type u for a concrete category. This is not marked as an instance as it could potentially apply to every type, and so is too expensive in typeclass search.
You can use it on particular examples as:
instance : has_coe_to_sort X := concrete_category.has_coe_to_sort X
Usually a bundled hom structure already has a coercion to function that works with different universes. So we don't use this as a global instance.
has_forget₂ C D, where C and D are both concrete categories, provides a functor forget₂ C D : C ⥤ C and a proof that forget₂ ⋙ (forget D) = forget C.
The forgetful functor C ⥤ D between concrete categories for which we have an instance has_forget₂ C .
In order to construct a “partially forgetting” functor, we do not need to verify functor laws; it suffices to ensure that compositions agree with forget₂ C D ⋙ forget D = forget C.