Sheaf categories are cartesian closed #
...if the underlying presheaf category is cartesian closed, the target category has (chosen) finite products, and there exists a sheafification functor.
instance
instCartesianClosedSheafOfHasSheafifyOfFunctorOpposite
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
(J : CategoryTheory.GrothendieckTopology C)
(A : Type u_2)
[CategoryTheory.Category.{u_4, u_2} A]
[CategoryTheory.HasSheafify J A]
[CategoryTheory.ChosenFiniteProducts A]
[CategoryTheory.CartesianClosed (CategoryTheory.Functor Cᵒᵖ A)]
: