Lean4
/-- The simplicial nerve of a simplicial category `C` is defined as the simplicial set whose
`n`-simplices are given by the set of simplicial functors from the simplicial thickening of
the linear order `Fin (n + 1)` to `C`
-/
noncomputable def SimplicialNerve (C : Type u) [Category.{v} C] [SimplicialCategory C] : SSet.{max u v}
where
obj n := EnrichedFunctor SSet (SimplicialThickening (ULift (Fin (n.unop.len + 1)))) C
map f := (SimplicialThickening.functor f.unop.toOrderHom.uliftMap).comp (E := C) SSet
map_id
i := by
change EnrichedFunctor.comp SSet (SimplicialThickening.functor (OrderHom.id)) = _
rw [SimplicialThickening.functor_id]
rfl
map_comp f
g :=
by
change
EnrichedFunctor.comp SSet
(SimplicialThickening.functor (f.unop.toOrderHom.uliftMap.comp g.unop.toOrderHom.uliftMap)) =
_
rw [SimplicialThickening.functor_comp]
rfl
