Commit 2024-04-07 17:14 3cb545c7

feat: existence of a limit in a concrete category implies smallness (#11625) In this PR, it is shown that if a functor G : J ⥤ C to a concrete category has a limit and that forget C is corepresentable, then G ⋙ forget C).sections is small. As the corepresentability property holds in many concrete categories (e.g. groups, abelian groups) and that we already know since #11420 that limits exist under the smallness assumption in such categories, then this lemma may be used in future PR in order to show that usual forgetful functors preserve all limits (regardless of universe assumptions). This shall be convenient in the development of sheaves of modules. In this PR, universes assumptions have also been generalized in the file Limits.Yoneda. In order to do this, a small refactor of the file Limits.Types was necessary. This introduces bijections like compCoyonedaSectionsEquiv (F : J ⥤ C) (X : C) : (F ⋙ coyoneda.obj (op X)).sections ≃ ((const J).obj X ⟶ F) with general universe parameters. In order to reduce imports in Limits.Yoneda, part of the file Limits.Types was moved to a new file Limits.TypesFiltered.