AB axioms in sheaf categories

If J is a Grothendieck topology on a small category C : Type v, and A : Type u₁ (with Category.{v} A) is a Grothendieck abelian category, then Sheaf J A is a Grothendieck abelian category.

instance CategoryTheory.Sheaf.instHasExactColimitsOfShapeOfHasFiniteLimitsOfPreservesColimitsOfShapeFunctorOppositeSheafToPresheaf {C : Type u} {A : Type u₁} {K : Type u₂} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} K] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.Limits.HasFiniteLimits A] [CategoryTheory.Limits.HasColimitsOfShape K A] [CategoryTheory.HasExactColimitsOfShape K A] [CategoryTheory.Limits.PreservesColimitsOfShape K (CategoryTheory.sheafToPresheaf J A)] : CategoryTheory.HasExactColimitsOfShape K (CategoryTheory.Sheaf J A)

instance CategoryTheory.Sheaf.instHasExactLimitsOfShapeOfHasFiniteColimitsOfPreservesFiniteColimitsFunctorOppositeSheafToPresheaf {C : Type u} {A : Type u₁} {K : Type u₂} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} K] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.HasWeakSheafify J A] [CategoryTheory.Limits.HasFiniteColimits A] [CategoryTheory.Limits.HasLimitsOfShape K A] [CategoryTheory.HasExactLimitsOfShape K A] [CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.sheafToPresheaf J A)] : CategoryTheory.HasExactLimitsOfShape K (CategoryTheory.Sheaf J A)

instance CategoryTheory.Sheaf.hasFilteredColimitsOfSize {C : Type u} {A : Type u₁} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v₁, u₁} A] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.HasSheafify J A] [CategoryTheory.Limits.HasFilteredColimitsOfSize.{v₂, u₂, v₁, u₁} A] : CategoryTheory.Limits.HasFilteredColimitsOfSize.{v₂, u₂, max u v₁, max (max (max u₁ u) v₁) v} (CategoryTheory.Sheaf J A)

instance CategoryTheory.Sheaf.hasExactColimitsOfShape {C : Type u} {A : Type u₁} {K : Type u₂} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} K] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.Limits.HasFiniteLimits A] [CategoryTheory.HasSheafify J A] [CategoryTheory.Limits.HasColimitsOfShape K A] [CategoryTheory.HasExactColimitsOfShape K A] : CategoryTheory.HasExactColimitsOfShape K (CategoryTheory.Sheaf J A)

instance CategoryTheory.Sheaf.ab5ofSize {C : Type u} {A : Type u₁} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v₁, u₁} A] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.Limits.HasFiniteLimits A] [CategoryTheory.HasSheafify J A] [CategoryTheory.Limits.HasFilteredColimitsOfSize.{v₂, u₂, v₁, u₁} A] [CategoryTheory.AB5OfSize.{v₂, u₂, v₁, u₁} A] : CategoryTheory.AB5OfSize.{v₂, u₂, max u v₁, max (max (max u₁ u) v₁) v} (CategoryTheory.Sheaf J A)

instance CategoryTheory.Sheaf.instIsGrothendieckAbelian {C : Type v} [CategoryTheory.SmallCategory C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₁) [CategoryTheory.Category.{v, u₁} A] [CategoryTheory.Abelian A] [CategoryTheory.IsGrothendieckAbelian A] [CategoryTheory.HasSheafify J A] : CategoryTheory.IsGrothendieckAbelian (CategoryTheory.Sheaf J A)