Commit 2025-08-18 09:17 6b45e68c

refactor(CategoryTheory/Limits): generalize universes for colimits of representables (#27576) Given a category C with Category.{v₁} C, this PR introduces a variant of the Yoneda embedding uliftYoneda.{w} : C ⥤ Cᵒᵖ ⥤ Type (max w v₁) which allows considering presheaves with values in higher universes. The study of left Kan extensions along the Yoneda embedding is generalized using this variant. This allows to generalize the definition of the singular set of a simplicial set and the singular homology of a topological space to arbitrary universes.