Commit 2023-10-18 08:18 e21dcf90

chore: make SimplexCategory.skeletalFunctor a functor to NonemptyFinLinOrdCat.{0} (#7272) SimplexCategory used to have a universe parameter, but for already some time, it is no longer the case. However, the functor SimplexCategory.skeletalFunctor was still a functor from the simplex category to NonemptyFinLinOrdCat.{v}. This PR changes this to NonemptyFinLinOrdCat.{0}. The main consequence of this is that if C is a category, the n-simplices of the simplicial set nerve C (see AlgebraicTopology.Nerve) are now definitionally equal to Fin (n+1) ⥤ C.