feat(category_theory/enriched): abstract enriched categories (#7175)

Enriched categories

We set up the basic theory of V-enriched categories, for V an arbitrary monoidal category. We do not assume here that V is a concrete category, so there does not need to be a "honest" underlying category! Use X ⟶[V] Y to obtain the V object of morphisms from X to Y. This file contains the definitions of V-enriched categories and V-functors. We don't yet define the V-object of natural transformations between a pair of V-functors (this requires limits in V), but we do provide a presheaf isomorphic to the Yoneda embedding of this object. We verify that when V = Type v, all these notion reduce to the usual ones.