Commit 2025-01-23 06:28 9c2a4e8e

feat(CategoryTheory): κ-filtered categories (#20005) If κ is a regular cardinal, we introduce the notion of κ-filtered category J: it means that any functor A ⥤ J from a small category such that Arrow A is of cardinality < κ admits a cocone. This generalizes the notion of filtered category. Indeed, we obtain the equivalence IsCardinalFiltered J ℵ₀ ↔ IsFiltered J. The API is mostly parallel to that of filtered categories.