warning: small refactor of simplicial categories

Stream: Infinity-Cosmos

[Joël Riou]

In mathlib PR #18175, I generalize the definition of simplicial categories to the situation we have a monoidal category V (which could be SSet), and on a type C, we have both a Category and a EnrichedCategory V C structure. The typeclass EnrichedOrdinaryCategory V C provides a bijection between types of morphisms in C in types of morphisms 𝟙_ V ⟶ (X ⟶[V] Y) in V. The phrasing I had chosen for simplicial categories works immediately in this more general situation, so that if some code breaks, the fix should be easy.

[Emily Riehl]

Thanks for the heads up. If you think of it, ping us again when this is merged, and I'll investigate whether anything needs fixing.