Finite simplicial sets are presentable

In this file, we show that finite simplicial sets are finitely presentable, which will allow the use of the small object argument in SSet.

instance SSet.Finite.instIsFinitelyPresentableObjSimplexCategoryStdSimplex (n : SimplexCategory) : CategoryTheory.IsFinitelyPresentable (stdSimplex.obj n)

theorem SSet.Finite.exists_epi_from_isCardinalPresentable (X : SSet) [X.Finite] : ∃ (Y : SSet) (_ : Y.Finite) (_ : CategoryTheory.IsFinitelyPresentable Y) (p : Y ⟶ X), CategoryTheory.Epi p

instance SSet.Finite.instIsFinitelyPresentable (X : SSet) [X.Finite] : CategoryTheory.IsFinitelyPresentable X