Possession of filtered colimits #
class
CategoryTheory.Limits.HasCofilteredLimitsOfSize
(C : Type u)
[CategoryTheory.Category.{v, u} C]
:
- 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.
Instances
class
CategoryTheory.Limits.HasFilteredColimitsOfSize
(C : Type u)
[CategoryTheory.Category.{v, u} C]
:
- 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.