(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]
: