A presheaf is a sheaf if and only if it satisfies some property

Question

I am having trouble with proving this statement:

$F$ is a sheaf if and only if for every presheaf $X$ and every dense presheaf $A$ of $X$, any arrow $A \to F$ has a unique extension to an arrow $X \to F$.

I have something for the $\impliedby$ direction but would appreciate it if someone could verify it, and am stumped by the $\implies$ direction.

$\impliedby$ Suppose $R$ is a covering sieve of $C$ and $(x_f \ | \ f \in R)$ is a compatible family on $F$ at $C$ or equivalently a morphism $R \to F$. We need to show there is a unique extension $y_C \to F$. If $R$ is a dense subpresheaf of $y_C$ this follows from the assumption. Let $f: D \to C$ be an element of $y_C(D)$. It is in $\bar{R}(D)$ precisely when $J_D(\phi_D(f)) = max(D)$ where $\phi$ is the subobject classifier of $R$ as subobject of $y_C$ and $J$ is the associated Lawvere-Tierney topology. This is the case precisely when $\phi_D(f) = \{g: E \to D \ | \ Rg(f) = gf \in R \}$ is covering. We note that $\phi_D(f) = f^*(R)$ which is covering by definition of a Grothendieck topology. This concludes this direction.

$\implies$ Let $X$ be a presheaf, $A$ a subpresheaf of $X$ such that $\bar{A} = X$ and $\mu: A \to F$ a natural transformation. Take some $x \in XC$. Then $x \in \bar{A}$, so $J_C(\phi_C(x)) = \max(C)$ which means that $\phi_C(x)$ is covering. Consider $(Xf(x) \ | \ f \in \phi_C(x))$. As $\phi_C(x) := \{f: D \to C \ | \ Xf(x) \in AC\}$, we have that this is a compatible family in $A$ at $C$. This is too nice to be coincidental, but I don't know what to do with this since $A$ is not (generally) a sheaf.

Answer 1

There's one typo in the first direction, it should be $\phi_D(f)=\{g\colon E\to D\mid y_Cg(f)=fg\in R\}$ (note the order of composition). Except that it looks good to me.

For the other direction I think we can "push" the compatible family $(Xf(x))_{f\in \phi_C(x)}$ to a compatible family in $F$ via $\mu$, which will have a unique amalgamation $x'\in FC$ as $F$ is a sheaf. The we define $X\to F$ by sending $x$ to $x'$. I haven't checked all the details but it seems like it should work.