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

- "Prove formally" by the Kan formula for $\text{Lan}_yA(F)$ that it is precisely the etale space of the sheaf $F$;
- "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.