Commit 2025-09-01 08:25 076c0cbb

feat(CategoryTheory/Enriched): the bicategory of V-enriched categories (#27129) This provides an instantiation of V-enriched categories as a bicategory. It also replaces the old definition of the category of enriched functors by a category that uses natural transformations between F.forget and G.forget as morphisms, as opposed to the previously used notion of enriched natural transformations.