Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
1 to 3 of 3
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 believe there is a fancy HIT in the metatheory that builds sheafification. However, I don’t think I ever wrote down the details.
Just for the record: Grothendieck’s plus construction works without choice; in fact, it can be formulated and used in the internal language of any topos. (I just added a very brief description of this to plus construction on presheaves.) However, it is still impredicative, as it refers to the collection of all subsets.
1 to 3 of 3