Mac Lane - Moerdijk's "Sheaves" gives this cryptic hint in page 91 that the equivalence between etale spaces and sheaves on a space $X$ can be cooked up using formal methods.


More precisely, we are in the following nerve-realization situation:
$$\begin{matrix}
\mathcal{O}(X)\xrightarrow{A}&\mathbf{Top}/X\\
\downarrow^y&\\
\mathbf{Set}^{\mathcal{O}(X)^{op}}
\end{matrix}$$


where the left Kan extension $\text{Lan}\_yA$ has a right adjoint $N\_A\colon \mathbf{Top}/X\to \mathbf{Set}^{\mathcal O(X)^\text{op}}$, which is defined precisely taking the (pre)sheaf of sections of $(p\colon E\to X)\in \mathbf{Top}/X$:


$$N\_A(p)\colon U\mapsto \mathbf{Top}/X\left(AU, p \right) = \mathbf{Top}/X\left(\left[\begin{smallmatrix} U \\ \downarrow \\ X\end{smallmatrix}\right], \left[\begin{smallmatrix} E \\ \downarrow \\ X\end{smallmatrix}\right] \right) = \{s\colon U\to E\mid ps\colon U\subseteq X\}$$


I am trying to work out the details of this construction, in particular I would like to


1. "Prove formally" by the Kan formula for $\text{Lan}\_yA(F)$ that it is precisely the etale space of the sheaf $F$;
2. "Prove formally" that this adjunction restricts to an equivalence $\mathbf{Sh}(X)\cong \mathbf{Et}(X)$ (this can be done appealing Lemma 4 right before page 91)


A nice consequence of adjoint nonsense would be that the reflection obtained in this way is also exact ($A$ commutes with finite limits, which exist in $\mathcal O(X)$).


I'm stuck in trying to make $\text{Lan}\_yA(F)$ an explicit object; one can appeal the Kan formula to obtain
$$
\text{Lan}\_yA(F)\cong\int^{U\colon \mathcal O(X)} FU\otimes AU
$$
where $\otimes$ denotes the canonical $\bf Set$-tensoring of ${\bf Top}/X$ which acts like $S\otimes \left[\begin{smallmatrix} E \\ \downarrow \\ X\end{smallmatrix}\right] = \left[\begin{smallmatrix} \coprod\_SE \\ \downarrow \\ X\end{smallmatrix}\right]$. The shape of colimits in $\mathbf{Top}/X$ gives that this space consists of $\left[\begin{smallmatrix} \big(\coprod\_U FU\times U\big)/\simeq \\ \downarrow \\ X\end{smallmatrix}\right]$ where I am modding out by a suitable equivalence relation. It would be nice to deduce that $\big(\coprod\_U FU\times U\big)/\simeq = \coprod\_{x\in X}F\_x$, with the topology...


Well, I'm beginning to suspect this is a too-painful alternative to the old explicit method. This is why I'm asking you if this can *really* be done.



Etale spaces using Kan extensions
[Initially I tried here to give a simplified version of a proof for 1. as given in Fourman & Scott's "Sheaves and logic" (Theorem 4.22 on page 356 of Springer LNM 753 "Applications of sheaves", proceedings of the 1977 Durham symposium). Then, having seen a comment above by Dimitri Chikhladze I realized I could use the universal property of the adjunction to further formalize a mighty portion of it.]


The key observation is that there is an isomorphism$$\mathcal O(E\_F)\cong\operatorname{Sub}(F)$$between the frame of opens of $E\_F:=$[the domain of]$\mathrm{Lan}\_yA(F)$ and the frame of subsheaves of $F$. Indeed$$\begin{multline\*}\mathcal O(E\_F)\cong\mathbf{Top}(E\_F,\mathbf2)\cong\mathbf{Top}/X\left(\mathrm{Lan}\_yA(F),\begin{smallmatrix}X\times\mathbf2\\\downarrow\\ X\end{smallmatrix}\right)\cong\mathbf{Set}^{\mathcal O(X)^\text{op}}\left(F,N\_A\left(\begin{smallmatrix}X\times\mathbf2\\\downarrow\\ X\end{smallmatrix}\right)\right)\\\cong\mathbf{Set}^{\mathcal O(X)^\text{op}}\left(F,\Omega\_{\mathbf{Sh}(X)}\right)=\mathbf{Sh}(X)\left(F,\Omega\_{\mathbf{Sh}(X)}\right)\cong\operatorname{Sub}(F),\end{multline\*}$$where $\mathbf2$ is the Sierpiński space and $\Omega\_{\mathbf{Sh}(X)}$ is the subobject classifier in sheaves.


The map $E\_F\to X$ in these terms is given by $\mathcal O(X)\cong\operatorname{Sub}(1)\xrightarrow{(F\to1)^{-1}}\operatorname{Sub}(F)\cong\mathcal O(E\_F)\ $ , i. e. by assigning to $V\in\mathcal O(X)$ the subsheaf $y(V)\times F\subseteq F$. It is then easy to see that this map is a local homeomorphism: the subsheaves $\xi(U):=\left\langle y(U)\rightarrowtail F\right\rangle$, one for each $\xi\in F(U)$ (the morphism is the one corresponding to $\xi$ by Yoneda) form a base of $\operatorname{Sub}(F)$ and for each of these the composite $\mathcal O(X)\to\operatorname{Sub}(F)\to\operatorname{Sub}(y(U))\cong\mathcal O(U)$ is $U\cap\\_$, so restriction to the open of $E\_F$ corresponding to this $\xi(U)$ is a homeomorphism onto its image.


Now observe that from what we've got, arbitrary sections of $E\_F\to X$ over opens correspond precisely to those subsheaves of $F$ which are subterminals. And by reverse Yoneda these are in one-to-one correspondence with elements $\xi\in F(U)$ for various $U$. (In other words, the base we described above exhausts all possible subterminal subsheaves of $F$.)


All this works if $X$ is sober. For a general $X$, the obtained $E\_F$ maps to $\operatorname{pt}(\mathcal O(X))$ instead of $X$. Fourman and Scott then pull this back along $X\to\operatorname{pt}(\mathcal O(X))$ and (easily) show that the result (is a local homeomorphism and) has the same supply of sections.


