Commit 2024-10-30 00:13 ef78db7e

refactor(CategoryTheory): simplicial categories are generalized to enriched "ordinary" categories (#18175) The API for simplicial categories is refactored. It fits more generally in the context of ordinary categories C (a type C and an instance [Category C]) that are also enriched over a monoidal category V (EnrichedCategory V C) in such a way that types of morphisms in C identify to types of morphisms 𝟙_ V ⟶ (X ⟶[V] Y) in V. This defines a new class EnrichedOrdinaryCategory, and SimplicialCategory is made an abbreviation for the particular case V is the category of simplicial sets.