Structures · Category theory
CategoryTheory.HasCardinalFilteredGenerator
The property that a category C and a regular cardinal κ
satisfy P.IsCardinalFilteredGenerators κ for a suitable essentially
small P : ObjectProperty C.
- Shape
- 2 explicit arguments · adds exists_generator
Extends1
Extended by2
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by7
- CategoryTheory.HasCardinalFilteredGenerator.exists_generator
- CategoryTheory.Adjunction.hasCardinalFilteredGenerator
- CategoryTheory.HasCardinalFilteredGenerator.exists_small_generator
- CategoryTheory.Equivalence.hasCardinalFilteredGenerator
- CategoryTheory.instEssentiallySmallIsCardinalPresentableOfHasCardinalFilteredGenerator
- CategoryTheory.HasCardinalFilteredGenerator.toLocallySmall
- CategoryTheory.HasCardinalFilteredGenerator.exists_equivalence