(Co)limits of the skeleton of a category #
The skeleton of a category inherits all (co)limits the category has.
Implementation notes #
Because the category instance of ThinSkeleton C comes from its Preorder instance, it is not the
case that HasLimits C iff HasLimits (ThinSkeleton C), as the homs live in different universes.
If this is something we really want, we should consider changing the category instance of
ThinSkeleton C.
instance CategoryTheory.Limits.hasLimitsOfShape_skeleton {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₂} [Category.{v₂, u₂} C] [HasLimitsOfShape J C] :
HasLimitsOfShape J (Skeleton C)
instance CategoryTheory.Limits.hasLimitsOfSize_skeleton {C : Type u₂} [Category.{v₂, u₂} C] [HasLimitsOfSize.{w, w', v₂, u₂} C] :
instance CategoryTheory.Limits.hasColimitsOfShape_skeleton {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₂} [Category.{v₂, u₂} C] [HasColimitsOfShape J C] :
HasColimitsOfShape J (Skeleton C)
instance CategoryTheory.Limits.hasLimitsOfShape_thinSkeleton {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₂} [Category.{v₂, u₂} C] [Quiver.IsThin C] [HasLimitsOfShape J C] :
HasLimitsOfShape J (ThinSkeleton C)
instance CategoryTheory.Limits.hasLimitsOfSize_thinSkeleton {C : Type u₂} [Category.{v₂, u₂} C] [Quiver.IsThin C] [HasLimitsOfSize.{w, w', v₂, u₂} C] :
instance CategoryTheory.Limits.hasColimitsOfShape_thinSkeleton {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u₂} [Category.{v₂, u₂} C] [Quiver.IsThin C] [HasColimitsOfShape J C] :