Categories with finite limits. #
A typeclass for categories with all finite (co)limits.
- out : ∀ (J : Type) [𝒥 : CategoryTheory.SmallCategory J] [inst : CategoryTheory.FinCategory J], CategoryTheory.Limits.HasLimitsOfShape J C
C
has all limits over any typeJ
whose objects and morphisms lie in the same universe and which hasFinType
objects and morphisms
A category has all finite limits if every functor J ⥤ C
with a FinCategory J
instance and J : Type
has a limit.
This is often called 'finitely complete'.
Instances
If C
has all limits, it has finite limits.
We can always derive HasFiniteLimits C
by providing limits at an
arbitrary universe.
- out : ∀ (J : Type) [𝒥 : CategoryTheory.SmallCategory J] [inst : CategoryTheory.FinCategory J], CategoryTheory.Limits.HasColimitsOfShape J C
C
has all colimits over any typeJ
whose objects and morphisms lie in the same universe and which hasFintype
objects and morphisms
A category has all finite colimits if every functor J ⥤ C
with a FinCategory J
instance and J : Type
has a colimit.
This is often called 'finitely cocomplete'.
Instances
We can always derive HasFiniteColimits C
by providing colimits at an
arbitrary universe.
- out : ∀ (J : Type) [inst : Fintype J], CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WidePullbackShape J) C
C
has all wide pullbacks any FintypeJ
HasFiniteWidePullbacks
represents a choice of wide pullback
for every finite collection of morphisms
Instances
- out : ∀ (J : Type) [inst : Fintype J], CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Limits.WidePushoutShape J) C
C
has all wide pushouts any FintypeJ
HasFiniteWidePushouts
represents a choice of wide pushout
for every finite collection of morphisms
Instances
Finite wide pullbacks are finite limits, so if C
has all finite limits,
it also has finite wide pullbacks
Finite wide pushouts are finite colimits, so if C
has all finite colimits,
it also has finite wide pushouts