Etale spaces using Kan extensions 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.
 A: I actually did exactly this when I taught a course on topos theory in Bonn.
See my lecture notes:
Lecture 3 and Lecture 4 here: http://www.math.ubc.ca/~carchedi/topos.html
I give a very detailed proof of 1. and 2. in these notes, using precisely the left Kan extension you describe as the definition, and then explicitly computing it, and arriving at precisely the classical definition of etale-space construction.
The course was for masters students, so everything is spelled out, but it could be slightly condensed.

Now that I have some extra time, let me give you some more details:
You asked how to deduce formally that the etale space of a sheaf $F$, as a set, is the disjoint union of its stalks. For this, make a couple observations:
1.) For each $x \in X,$ the functor $Set^{\mathcal{O}\left(X\right)^{op}}\to Set$ sending $F$ to $F_x$ is colimit preserving (one way of seeing this is that if $i_x:\mathcal{O}\left(X\right)_x \hookrightarrow \mathcal{O}\left(X\right)$ is the inclusion of the poset of open neighborhoods of $x$ into all open subsets of $X$, $F_x$ is simply the colimit of $F \circ i_x.$
2.) The composite $$Set^{\mathcal{O}\left(X\right)^{op}} \stackrel{A}{\longrightarrow} \mathbf{Top}/X \to Set/X \stackrel{\sim}{\longrightarrow} Set^{X} \stackrel{ev_x}{\longrightarrow} Set$$ is colimit preserving. (Also notice that the composite $Set/X \stackrel{\sim}{\longrightarrow} Set^{X} \stackrel{ev_x}{\longrightarrow} Set$ sends a map $Y \to X$ to its fiber $Y_x$ over $x.$) 
A simple check shows that both functors agree on representables, that is, the fiber of $U \hookrightarrow X$ over $x$ is exactly the stalk $y(U)_x$ of the representable sheaf.
It hence follows that the underlying set of the etale space of $F$ is the disjoint union of its stalks. It also follows that the topology is the final topology with respect to all maps of the form $U \to \coprod F_x$ sending $y \mapsto germ_y \lambda$ for $\lambda \in F\left(U\right)$, and one can show pretty easily that this topology maps the map down to $X$ a local homeomorphism. One can also check that the unit of the adjunction induced by $A$ is an iso precisely on sheaves, and the co-unit is an iso precisely on local homeomorphisms into $X$. You can see http://www.math.ubc.ca/~carchedi/Lecture4.pdf for the glorious details.
A: [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.
