Structures · Category theory
CategoryTheory.Limits.HasCofilteredLimitsOfSize
Class for having all cofiltered limits of a given size.
- Defined in
- Mathlib.CategoryTheory.Limits.Filtered
- Shape
- One type argument · adds HasLimitsOfShape
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- CategoryTheory.Functor
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by12
- CategoryTheory.Limits.hasCofilteredLimitsOfSize_of_univLE
- CategoryTheory.Limits.hasProducts_of_finite_and_cofiltered
- CategoryTheory.Limits.hasCofilteredLimitsOfSize_shrink
- CategoryTheory.AB5StarOfSize_of_univLE
- CategoryTheory.Limits.instHasCofilteredLimitsOfSizeFunctor
- CategoryTheory.Limits.HasCofilteredLimitsOfSize.HasLimitsOfShape
- CategoryTheory.AB5StarOfSize_shrink
- CategoryTheory.AB4Star.of_AB5Star
- CategoryTheory.Limits.has_filtered_colimits_op_of_has_cofiltered_limits
- CategoryTheory.Limits.has_filtered_colimits_of_has_cofiltered_limits_op
- CategoryTheory.Limits.has_limits_of_finite_and_cofiltered
- CategoryTheory.Limits.hasLimitsOfShape_of_has_cofiltered_limits
Ancestors0
No ancestors.