canonical functor into sheaves

Stream: Is there code for X?

[Anthony Bordg]

Is the canonical functor, i.e. the Yoneda embedding composed with the sheafification functor, defined in mathlib4?
The Yoneda embedding is CategoryTheory.yoneda, but for the sheafification functor I only found CategoryTheory.sheafification, which has values into a category of presheaves, not a category of sheaves.

[Adam Topaz]

We have docs#CategoryTheory.presheafToSheaf

[Adam Topaz]

and, of course, its adjoint docs#CategoryTheory.sheafToPresheaf