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_reducible]

noncomputable instance instMonoidalClosedSheafOfHasSheafifyOfFunctorOpposite {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u_2) [CategoryTheory.Category.{v_2, u_2} A] [CategoryTheory.HasSheafify J A] [CategoryTheory.CartesianMonoidalCategory A] [CategoryTheory.MonoidalClosed (CategoryTheory.Functor Cᵒᵖ A)] : CategoryTheory.MonoidalClosed (CategoryTheory.Sheaf J A)

Equations

• One or more equations did not get rendered due to their size.