Commit 2024-03-29 21:36 b5cf43ef

feat(AlgebraicTopology): the monoidal category structure on simplicial sets (#11396) If a category C has chosen finite products, then the functor category J ⥤ C also. In particular, the category of simplicial sets is endowed with the monoidal category given by the explicit terminal object and binary products. Simplifications lemmas have also been added in the context of categories with chosen finite products. For terminal objects in such categories, the terminal object is given as a limit cone of Functor.empty.{0} C rather than Functor.empty.{v} C so as to be consistent with the limits API for terminal objects.