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?

]]>I have added a brief note about type-theoretic polymorphism to the list of impredicative axioms at predicative mathematics.

]]>Should the predicate $\Diamond$ on a formal topology be regarded as making it into an overt space?

]]>