Filtered categories and limits #
In this file , we show that C
is filtered if and only if for every functor F : J ⥤ C
from a
finite category there is some X : C
such that lim Hom(F·, X)
is nonempty.
Furthermore, we define the type classes HasCofilteredLimitsOfSize
and HasFilteredColimitsOfSize
.
C
is filtered if and only if for every functor F : J ⥤ C
from a finite category there is
some X : C
such that lim Hom(F·, X)
is nonempty.
Lemma 3.1.2 of [KS06]
C
is cofiltered if and only if for every functor F : J ⥤ C
from a finite category there is
some X : C
such that lim Hom(X, F·)
is nonempty.
Class for having all cofiltered limits of a given size.
For all filtered types of size
w
, we have limits
Instances
Class for having all filtered colimits of a given size.
For all filtered types of a size
w
, we have colimits
Instances
Class for having cofiltered limits.
Equations
Instances For
Class for having filtered colimits.