Structures · Category theory
CategoryTheory.Limits.HasIterationOfShape
A category C has iterations of shape a linearly ordered type J
when certain specific shapes of colimits exists: colimits indexed by J,
and by Set.Iio j for j : J.
- Shape
- 2 explicit arguments · adds hasColimitsOfShape_of_isSuccLimit, hasColimitsOfShape
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- Set.Elem
How is a type an instance?
Loading the hierarchy index…
Assumed by88
- CategoryTheory.SmallObject.SuccStruct.Iteration.F
- CategoryTheory.SmallObject.SuccStruct.iterationFunctor
- CategoryTheory.SmallObject.SuccStruct.arrowι
- CategoryTheory.SmallObject.SuccStruct.Iteration.mapObj
- CategoryTheory.OrthogonalReflection.iteration
- CategoryTheory.SmallObject.SuccStruct.iteration
- CategoryTheory.SmallObject.SuccStruct.Iteration.congr_obj
- CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.inductiveSystem
- CategoryTheory.OrthogonalReflection.iterationObjSuccIso
- CategoryTheory.SmallObject.SuccStruct.transfiniteCompositionOfShapeιIteration
- CategoryTheory.SmallObject.SuccStruct.Iteration.trunc
- CategoryTheory.SmallObject.SuccStruct.ιIteration
- CategoryTheory.Limits.hasColimitsOfShape_of_isSuccLimit
- CategoryTheory.OrthogonalReflection.reflectionObj
- CategoryTheory.SmallObject.SuccStruct.iterationFunctorObjSuccIso
- CategoryTheory.OrthogonalReflection.iteration_map_succ
- CategoryTheory.SmallObject.SuccStruct.iterationCocone
- CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.functor
- CategoryTheory.OrthogonalReflection.transfiniteCompositionOfShapeReflection
- CategoryTheory.SmallObject.SuccStruct.Iteration.arrowSucc_eq
- CategoryTheory.OrthogonalReflection.reflection
- CategoryTheory.SmallObject.SuccStruct.Iteration.congr_map
- CategoryTheory.SmallObject.SuccStruct.iter
- CategoryTheory.SmallObject.SuccStruct.prop_iterationFunctor_map_succ
- CategoryTheory.SmallObject.SuccStruct.iterationFunctor_map_succ
- CategoryTheory.Limits.HasIterationOfShape.hasColimitsOfShape_of_isSuccLimit
- CategoryTheory.Limits.hasColimitsOfShape_of_initialSeg
- CategoryTheory.OrthogonalReflection.corepresentableBy
- CategoryTheory.SmallObject.SuccStruct.Iteration.mapObj_trans
- CategoryTheory.SmallObject.SuccStruct.Iteration.arrow_mk_mapObj
- CategoryTheory.OrthogonalReflection.iteration_map_succ_injectivity
- CategoryTheory.OrthogonalReflection.isRightAdjoint_ι
- CategoryTheory.Limits.hasColimitsOfShape_of_isSuccLimit'
- CategoryTheory.SmallObject.SuccStruct.Iteration.congr_arrowMap
- CategoryTheory.SmallObject.SuccStruct.isColimitIterationCocone
- CategoryTheory.SmallObject.SuccStruct.Iteration.arrowMap_limit
- CategoryTheory.SmallObject.SuccStruct.iterationFunctorObjBotIso
- CategoryTheory.OrthogonalReflection.iteration_map_succ_surjectivity
- CategoryTheory.Limits.instPreservesWellOrderContinuousOfShapeFunctorObjEvaluationOfHasIterationOfShape
- CategoryTheory.SmallObject.SuccStruct.iterationFunctor.congr_simp
- CategoryTheory.SmallObject.SuccStruct.Iteration.obj_succ
- CategoryTheory.OrthogonalReflection.isLocal_isLocal_reflection
- CategoryTheory.Limits.instPreservesWellOrderContinuousOfShapeArrowRightFuncOfHasIterationOfShape
- CategoryTheory.SmallObject.SuccStruct.Iteration.nonempty
- CategoryTheory.Limits.hasIterationOfShape_of_initialSeg
- CategoryTheory.OrthogonalReflection.iterationObjSuccIso.congr_simp
- CategoryTheory.SmallObject.SuccStruct.iterationFunctorObjSuccIso.congr_simp
- CategoryTheory.Limits.instHasIterationOfShapeArrow
- CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfBot
- CategoryTheory.SmallObject.SuccStruct.Iteration.obj_bot
Ancestors0
No ancestors.