Commit 2024-10-30 00:13 ef78db7e
View on Github →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.