Axiom of choice in sheafification?

Question

Let $(\mathbb{C}, J)$ be a small site, and let $F : \mathbb{C}^{\mathsf{op}} \to \mathsf{Set}$ be a separated presheaf with respect to $(\mathbb{C}, J)$. In the usual proof that $F^+ : \mathbb{C}^\mathsf{op} \to \mathsf{Set}$ is a sheaf, for example in the book by Mac Lane and Moerdijk, one considers a cover $R \in J(C)$ for an object $C$ of $\mathbb{C}$ and a matching family of elements $\left(\mathbf{x}_f \in F^+(\mathsf{dom}(f))\right)_{f \in R}$. To construct the amalgamation of this matching family, one then chooses a representative from each equivalence class $\mathbf{x}_f$, and then defines an amalgamation in terms of these representatives. It therefore seems that this argument requires a certain use of the axiom of choice; not necessarily the full-blown axiom of choice, but the axiom of choice restricted to sets below a certain cardinality (presumably the cardinality of the set of arrows of $\mathbb{C}$). Is this analysis correct? I.e. does this (standard) proof that $F^+$ is a sheaf if $F$ is separated involve (a restricted version of) the axiom of choice?

Answer 1

You can show $F^+$ is a sheaf when $F$ is separated just using collection, without the axiom of choice. See, for example, claim 2 of theorem 4.2 in Van den Berg & Moerdijk, Aspects of predicative algebraic set theory III: sheaves (arXiv link). Although I guess some of the standard presentations do (unnecessarily) use choice, as you point out.

Also in chapter V of Moedijk and Mac Lane there is a second construction of sheafification for Lawvere-Tierney topologies, which include Grothendieck topologies as a special case, and works in arbitrary elementary toposes, so does not require choice.