Connecting the two different `sheafify`

Stream: Is there code for X?

[Heather Macbeth]

There are definitions docs#CategoryTheory.GrothendieckTopology.sheafify and docs#TopCat.Presheaf.sheafify, and I assume (?) they are supposed to give the same thing (mathematically, if not definitionally) in the case of a sheaf of types on a topological space. But it seems not to be done -- is that right?

[Junyan Xu]

It's a to-do item to build the forget-sheafification adjunction in the TopCat setting. Once that's done, it should be easy from
docs#CategoryTheory.sheafificationAdjunction and docs#CategoryTheory.Adjunction.leftAdjointUniq
(docs#TopCat.Sheaf.forget is defeq to docs#CategoryTheory.sheafToPresheaf)

[Heather Macbeth]

Thanks! I would be very happy to see that to-do item done ...

If I understand correctly, this plan would show that the two sheafify operations are naturally isomorphic. I suppose they're not defeq?

[Adam Topaz]

They won't be defeq.