Structures · Category theory
CategoryTheory.MorphismProperty.IsCardinalForSmallObjectArgument
Given I : MorphismProperty C and a regular cardinal κ : Cardinal.{w},
this property asserts the technical conditions which allow to proceed
to the small object argument by doing a construction by transfinite
induction indexed by the well-ordered type κ.ord.ToType.
- Shape
- 2 explicit arguments · adds isSmall, locallySmall, hasPushouts, hasCoproducts, hasIterationOfShape, preservesColimit
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- SSet
How is a type an instance?
Loading the hierarchy index…
Assumed by66
- CategoryTheory.SmallObject.obj
- CategoryTheory.SmallObject.ιObj
- CategoryTheory.SmallObject.πObj
- CategoryTheory.SmallObject.ιIteration
- CategoryTheory.SmallObject.objMap
- CategoryTheory.SmallObject.iterationFunctor
- CategoryTheory.SmallObject.iteration
- CategoryTheory.SmallObject.hasColimitsOfShape_discrete
- CategoryTheory.SmallObject.hasPushouts
- CategoryTheory.SmallObject.iterationFunctorMapSuccAppArrowIso
- CategoryTheory.SmallObject.functorialFactorizationData
- CategoryTheory.SmallObject.iterationFunctorObjObjRightIso
- CategoryTheory.SmallObject.relativeCellComplexιObj
- CategoryTheory.SmallObject.llp_rlp_of_isCardinalForSmallObjectArgument'
- CategoryTheory.SmallObject.succStruct
- CategoryTheory.SmallObject.transfiniteCompositionOfShapeιIterationAppRight
- CategoryTheory.SmallObject.relativeCellComplexιObjFObjSuccIso
- CategoryTheory.SmallObject.transfiniteCompositionsOfShape_ιObj
- CategoryTheory.SmallObject.locallySmall
- CategoryTheory.SmallObject.πObj_ιIteration_app_right
- CategoryTheory.SmallObject.llp_rlp_of_isCardinalForSmallObjectArgument_aleph0
- CategoryTheory.SmallObject.isSmall
- CategoryTheory.SmallObject.iterationFunctorObjObjRightIso_ιIteration_app_right
- CategoryTheory.SmallObject.ιObj_πObj
- CategoryTheory.SmallObject.transfiniteCompositionOfShapeSuccStructPropιIteration
- CategoryTheory.MorphismProperty.IsCardinalForSmallObjectArgument.hasIterationOfShape
- CategoryTheory.MorphismProperty.IsCardinalForSmallObjectArgument.preservesColimit
- CategoryTheory.MorphismProperty.IsCardinalForSmallObjectArgument.isSmall
- CategoryTheory.SmallObject.preservesColimit
- CategoryTheory.SmallObject.hasRightLiftingProperty_πObj
- CategoryTheory.SmallObject.ιObj_naturality
- CategoryTheory.SmallObject.πObj_naturality
- CategoryTheory.SmallObject.rlp_πObj
- CategoryTheory.SmallObject.llp_rlp_of_isCardinalForSmallObjectArgument
- CategoryTheory.MorphismProperty.IsCardinalForSmallObjectArgument.locallySmall
- CategoryTheory.SmallObject.iterationFunctorMapSuccAppArrowIso_hom_right_right_comp
- CategoryTheory.SmallObject.hasCoproducts
- CategoryTheory.MorphismProperty.IsCardinalForSmallObjectArgument.hasCoproducts
- CategoryTheory.SmallObject.iterationFunctorMapSuccAppArrowIso_hom_right_right_comp_assoc
- CategoryTheory.SmallObject.iterationObjRightIso
- CategoryTheory.SmallObject.hasIterationOfShape
- CategoryTheory.SmallObject.objMap_comp
- CategoryTheory.SmallObject.πFunctorObj_eq
- CategoryTheory.MorphismProperty.IsCardinalForSmallObjectArgument.hasPushouts
- CategoryTheory.SmallObject.ιFunctorObj_eq
- CategoryTheory.SmallObject.functorialFactorizationData_p_app
- CategoryTheory.SmallObject.functorialFactorizationData_Z_obj
- CategoryTheory.SmallObject.instIsIsoRightAppArrowMapToTypeOrdFunctorIterationFunctor
- CategoryTheory.SmallObject.iterationFunctorObjObjRightIso_ιIteration_app_right_assoc
- CategoryTheory.SmallObject.functorialFactorizationData_i_app
Ancestors0
No ancestors.