Possession of filtered colimits

class CategoryTheory.Limits.HasCofilteredLimitsOfSize (C : Type u) [CategoryTheory.Category.{v, u} C] : Prop

• HasLimitsOfShape : ∀ (I : Type w) [inst : CategoryTheory.Category.{w', w} I] [inst_1 : CategoryTheory.IsCofiltered I], CategoryTheory.Limits.HasLimitsOfShape I C

  For all filtered types of size w, we have limits

Class for having all cofiltered limits of a given size.

class CategoryTheory.Limits.HasFilteredColimitsOfSize (C : Type u) [CategoryTheory.Category.{v, u} C] : Prop

• HasColimitsOfShape : ∀ (I : Type w) [inst : CategoryTheory.Category.{w', w} I] [inst_1 : CategoryTheory.IsFiltered I], CategoryTheory.Limits.HasColimitsOfShape I C

  For all filtered types of a size w, we have colimits

Class for having all filtered colimits of a given size.

instance CategoryTheory.Limits.hasLimitsOfShape_of_has_cofiltered_limits {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCofilteredLimitsOfSize.{w', w, v, u} C] (I : Type w) [CategoryTheory.Category.{w', w} I] [CategoryTheory.IsCofiltered I] : CategoryTheory.Limits.HasLimitsOfShape I C

instance CategoryTheory.Limits.hasColimitsOfShape_of_has_filtered_colimits {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFilteredColimitsOfSize.{w', w, v, u} C] (I : Type w) [CategoryTheory.Category.{w', w} I] [CategoryTheory.IsFiltered I] : CategoryTheory.Limits.HasColimitsOfShape I C