Structures · Category theory
CategoryTheory.IsCardinalAccessibleCategory
Given a regular cardinal κ, a category C is κ-accessible
if it has κ-filtered colimits 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.CardinalDirectedPoset
How is a type an instance?
Loading the hierarchy index…
Assumed by8
- CategoryTheory.isCardinalFilteredGenerator_isCardinalPresentable
- CategoryTheory.Equivalence.isCardinalAccessibleCategory
- CategoryTheory.Adjunction.isCardinalAccessibleCategory
- Cardinal.SharplyLT.exists_cofinal_of_isCardinalAccessibleCategory_cardinalDirectedPoset
- CategoryTheory.IsCardinalAccessibleCategory.instIsDenseFullSubcategoryIsCardinalPresentableι
- CategoryTheory.IsCardinalAccessibleCategory.instIsCardinalFilteredCostructuredArrowFullSubcategoryIsCardinalPresentableι
- CategoryTheory.IsCardinalAccessibleCategory.toHasCardinalFilteredGenerator
- CategoryTheory.IsCardinalAccessibleCategory.toHasCardinalFilteredColimits