Indeed, in order to obtain the monoidal structure on categories of sheaves with values in a closed symmetric monoidal category (with suitable limits), using #12728, we will need to know that if Y is any presheaf, and f : X₁ ⟶ X₂ is a morphism of presheaves which becomes an isomorphism after sheafification, then it is also the case of f ▷ Y. This is equivalent to saying that if Z is any sheaf, the induced map (X₂ ⊗ Y ⟶ Z) → (X₁ ⊗ Y ⟶ Z) is a bijection, which is the same as showing there is a bijection (X₂ ⟶ Y ⟹ Z) → (X₁ ⟶ Y ⟹ Z) (if I use the notation ⟹ for the internal hom of presheaves), and we may conclude if we know that Y ⟹ Z is a sheaf when Z is a sheaf (see Sites.SheafHom for a similar result). Finally, using your result in PR #15894, we may also get that the monoidal category structure on sheaves is also closed.

In order to get the tensor product of sheaves (with its monoidal compatibilites), we not only need to know that the monoidal structure on presheaves is closed, but we also need a certain understanding of what the sections of Y ⟹ Z look like. Then, I am not sure what to do with this PR, because on the one hand, your proof is really great, but we may not extract enough information out of it for our future applications. Another approach would be to develop the more explicit construction in a way that would allow both a construction of a MonoidalClosed instance, and working with a preexistent MonoidalClosed instance, e.g. the one given by this PR? In which case, the API would provide isomorphisms with the given ihom.

I don't have a strong opinion on whether to merge this or not. If nothing else, I think it's a cool application of the adjoint lifting theorem. But you're right that it's not good enough to get the monoidal structure on sheaves. However, I don't think it hurts to have different definitions of MonoidalClosed for functor categories (there is already one for functors out of a groupoid), as long as they are defs and only turned on as instances locally. These structures are unique up to isomorphism as you note and it will always be easy to relate them.

What's the status of the explicit decsription of internal homs of presheaves? IIRC, you had some WIP code on a branch doing this?

I have done the first step in #18009 which together with #17326 gives an enrichment of a functor category J ⥤ C in C. In a certain sense, this is the "global sections" of the expected internal hom. Then, in order to construct the actual internal hom, I will study the functoriality of this enrichement of J ⥤ C with respect to the category J. Then, all the enrichements of Under j ⥤ C for j : J over C should give the expected enrichment of J ⥤ C in itself, and hopefully it will be possible to deduce that J ⥤ C is closed monoidal.

I've reviewed the two PRs that #18009 depends on.

I feel the best solution is to merge this one.