Commit 2025-01-24 08:30 21e96d4e

feat(CategoryTheory): (co)limits indexed by preorders (#20335) In this PR, we show very basic results about (co)limits indexed by a preordered type J. OrderBot J implies the existence of all limits indexed by J (and similarly when J has a greatest element). We also introduce the typeclass HasIterationOfShape C J which contains the assumptions in order to do constructions by transfinite induction (see #20245 for the application to the small object argument).