This is basically a reference request: It was recently pointed out to me that the construction and correctness of the sheafification functor (in the context of 1-topos theory) depends on either the axiom of choice (using Grothendieck’s ++-construction or variations thereof) or impredicativity (using Lawvere’s construction).

Do any of you know a place where sheafification is discussed relative to a constructive, predicative metatheory without any choice?

I’m aware of Moerdijk and Palmgren’s: Type theories, toposes and constructive set theory: predicative aspects of AST. There sheafification is constructed for “collection sites”, but I don’t think there are many infinitary collection sites without assuming AMC. Maybe I’m wrong?

For coherent sites, there’s no problem, as only finite choice is needed. I’m interested primarily in the case of sites with countable covers.

A big hammer (if we have it?) might be to say that in the internal logic of the presheaf topos, sheafification is a localization and could presumably be done with an internal localization HIT (which we have if we have inductive types in the meta-theory?) Or perhaps there’s directly a fancy HIT in the metatheory that builds sheafification?

]]>The sheafification of a (1-)presheaf on a site is classically constructed in a two-step process $X^{++}$, where $X^+$ consists of matching families in $X$, is always separated, and is a sheaf if $X$ is separated. But the sheafification can also be constructed in a single step by looking at matching families over *hypercovers*. However, the only published reference I can find which mentions this latter fact is *Higher Topos Theory* (section 6.5.3), and it doesn’t really give a proof. Does anyone know of a reference on “good old” 1-sheaves which discusses sheafification via hypercovers?