$\def\et{\operatorname{\acute Et}} \def\sh{\operatorname{Sh}} \def\set{\mathsf{Set}} \def\top{\mathsf{Top}} \def\psh{\operatorname{PSh}} $From a google search, it appears to be a well-known fact that there is an equivalence of categories $\et(X)\simeq\sh_\set(X)$, where $X$ is a topological space. This equivalence of categories is induced by the pair of anti-parallel functors $\top/X\to\psh_\set(X)$ that sends a topological space over $X$ to its sheaf of continuous sections, and $\psh_\set(X)\to\top/X$, that sends a presheaf of sets over $X$ to the étale space of the presheaf. The essential image of the former are sheaves over $X$, whereas the essential image of the latter are étale spaces (local homeomorphisms) over $X$.
However, I have been unable to find a complete proof of the equivalence $\et(X)\simeq\sh_\set(X)$. I know that it is not hard to define the action on morphisms of these two functors, to show that all the constructions are well-defined and to work out the rest of the details. This can be done as an exercise by anyone learning about sheaves. Nevertheless, I was curious to know about some source that actually writes the full proof, making explicit all the details involved. I haven't found anything on the Stacks Project, nor on Kashiwara-Schapira Categories and Sheaves, or on the nLab.
I was thinking that maybe it isn't written anywhere because it may follow from more general results. I know nothing about abstract nonsense like sites, Grothendieck topologies or toposes. I don't know if the equivalence is just a corollary or a particular case from a more general idea coming out from there.
So my questions are:
- Do you know about some source where the full proof of the equivalence is worked out?
- Do you know if the equivalence follows naturally from a more general or more abstract result?
This is Corollary II.3 on p. 90 of MacLane and Moerdijk's "Sheaves in Geometry and Logic". Chapter II does not yet require the theory of Grothendieck topoi.