AB axioms in the category of ind-objects #
We show that Ind C satisfies Grothendieck's axiom AB5 if C has finite limits.
instance
CategoryTheory.Limits.instHasExactColimitsOfShapeIndOfHasFiniteLimits
{C : Type u}
[Category.{v, u} C]
{J : Type v}
[SmallCategory J]
[IsFiltered J]
[HasFiniteLimits C]
:
HasExactColimitsOfShape J (Ind C)
instance
CategoryTheory.Limits.instAB5IndOfHasFiniteLimits
{C : Type u}
[Category.{v, u} C]
[HasFiniteLimits C]
: