Structures · Category theory
CategoryTheory.IsCardinalLocallyPresentable
Given a regular cardinal κ, a category C is κ-locally presentable
if it is cocomplete and admits a (small) family G : ι → C of κ-presentable
objects such that any object identifies as a κ-filtered colimit of these objects.
- Shape
- 2 explicit arguments
Extends2
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- CategoryTheory.Functor
How is a type an instance?
Loading the hierarchy index…
Assumed by8
- CategoryTheory.Adjunction.isCardinalLocallyPresentable
- CategoryTheory.Equivalence.isCardinalLocallyPresentable
- CategoryTheory.MorphismProperty.isLocallyPresentable_isLocal
- CategoryTheory.IsCardinalLocallyPresentable.toHasColimitsOfSize
- CategoryTheory.instIsCardinalAccessibleCategoryOfIsCardinalLocallyPresentable
- CategoryTheory.IsCardinalLocallyPresentable.of_le
- CategoryTheory.IsCardinalLocallyPresentable.toHasCardinalFilteredGenerator
- CategoryTheory.Presheaf.instIsCardinalLocallyPresentableFunctorOppositeOfHasPullbacks