# Commit 2021-05-01 00:19 b88a9d14

View on Github →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.