Showing that the sheaf-functor $\epsilon: \tilde{\sf C} \to \tilde{\tilde{\sf C}}$ is an equivalence

Question

Let $(\mathsf C,J)$ be a site. Then we have the category of sheaves $\tilde{\mathsf C}$ and the category $\tilde{\tilde{\sf C}}$ of sheaves over $\tilde{\sf C}$ (both considered with the canonical topology).

There is a functor $\epsilon: \tilde{\sf C} \to \tilde{\tilde{\sf C}}$, which is the composition $\bf ay$ of the Yoneda functor $\mathbf y_C = \operatorname{Hom}(-,C)$ and the associated sheaf functor $\mathbf a$.

I have seen it repeatedly claimed that $\epsilon$ is an equivalence, but I lack background to understand the proof in the Elephant (C2.2.7). Nonetheless, Makkai and Reyes claim in First Order Categorical Logic that "it is not hard to show Lemma 1.3.14 directly" (where 1.3.14 is the statement that $\epsilon$ is an equivalence).

---

So I tried to prove it directly; obviously the difficulty lies in defining the functor $R$ that forms an equivalence together with $\epsilon$. Here is my attempt:

Let $\mathcal S$ be a sheaf over $\tilde{\sf C}$ (so an object of $\tilde{\tilde{\sf C}}$); then $\mathcal S = \varinjlim_i \operatorname{Hom}(-,F_i)$ for some objects $F_i$ of $\tilde{\sf C}$. For any $F$, now, $\mathcal SF$ is an equivalence class of natural transformations $[\eta: F \to F_i]$. So now I let:

$$R\mathcal S = G, GC = \left\{\left([\eta_C: FC \to F_iC],x\right) \mid F \in \operatorname{ob}\tilde{\sf C}, x \in FC\right\}$$

and for $f:D \to C$, define $Gf: GC \to GD$ by $$Gf([\eta_C:FC\to F_iC],x) = ([\eta_D:FD \to F_iD],Ff(x))$$

So I think this will provide an equivalence, but I'm not really sure because of the multitude of supposedly obvious claims (e.g. about well-definedness, and that $G$ is a sheaf).

---

My question now has two parts:

1. Is this definition going to work? What should I pay careful attention to?
2. If not, is there any other explicit construction of the functor $R$?

Answer 1

For simplicity, assume $(\mathbb{C}, J)$ is a small subcanonical site. The quasi-inverse of the embedding $\mathbf{Sh}(\mathbb{C}, J) \to \mathbf{Sh}(\mathbf{Sh}(\mathbb{C}, J))$ has a very simple description: it is the functor that sends a sheaf $F : \mathbf{Sh}(\mathbb{C}, J)^\mathrm{op} \to \mathbf{Set}$ to its restriction along the embedding $\mathbb{C} \to \mathbf{Sh}(\mathbb{C}, J)$.

Indeed, suppose $F : \mathbf{Sh}(\mathbb{C}, J)^\mathrm{op} \to \mathbf{Set}$ is a sheaf. I claim $F$ is determined up to unique isomorphism by its restriction along the embedding $\mathbb{C} \to \mathbf{Sh}(\mathbb{C}, J)$. Indeed, let $X : \mathbb{C}^\mathrm{op} \to \mathbf{Set}$ be a $J$-sheaf. Then $X$ is the colimit of a canonical small diagram of representable sheaves on $(\mathbb{C}, J)$ in a canonical way. Consider the colimiting cocone on $X$: it is a universal effective epimorphic family and is therefore a covering family in the canonical topology on $\mathbf{Sh}(\mathbb{C}, J)$. Thus, $F (X)$ is indeed determined up to unique isomorphism by the restriction of $F$ to $\mathbb{C}$. We must also show that the restriction is actually a sheaf on $(\mathbb{C}, J)$; but this is true because $J$-covering sieves in $\mathbb{C}$ become universal effective epimorphic families in $\mathbf{Sh}(\mathbb{C}, J)$.

Thus we obtain a functor $\mathbf{Sh}(\mathbf{Sh}(\mathbb{C}, J)) \to \mathbf{Sh}(\mathbb{C}, J)$ that is left quasi-inverse to the embedding $\mathbf{Sh}(\mathbb{C}, J) \to \mathbf{Sh}(\mathbf{Sh}(\mathbb{C}, J))$, and the argument above shows that it is also a right quasi-inverse.