The category of simplicial objects is simplicial #
In CategoryTheory.Functor.FunctorHom
, it was shown that a category of functors
C ⥤ D
is enriched over a suitable category C ⥤ Type _
of functors to types.
In this file, we deduce that SimplicialObject D
is enriched over SSet.{v} D
(when D : Type u
and [Category.{v} D]
) and that SimplicialObject D
is actually a simplicial category. In particular, the category of simplicial
sets is a simplicial category.
noncomputable instance
CategoryTheory.SimplicialObject.instEnrichedCategorySSet
{D : Type u}
[CategoryTheory.Category.{v, u} D]
:
Equations
- One or more equations did not get rendered due to their size.
noncomputable instance
CategoryTheory.SimplicialObject.instSimplicialCategory
{D : Type u}
[CategoryTheory.Category.{v, u} D]
:
Equations
- CategoryTheory.SimplicialObject.instSimplicialCategory = CategoryTheory.SimplicialCategory.mk (fun (K L : CategoryTheory.SimplicialObject D) => CategoryTheory.Functor.natTransEquiv.symm) ⋯ ⋯