mathlib

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

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. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>