Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorUlrik
   • CommentTimeNov 21st 2016
   • PermaLink
   Author: Ulrik
   Format: MarkdownItexThis 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](http://dx.doi.org/10.1016/S0168-0072(01)00079-3). 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?

   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?

2. • CommentRowNumber2.
   • CommentAuthorMike Shulman
   • CommentTimeNov 21st 2016
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI believe there is a fancy HIT in the metatheory that builds sheafification. However, I don't think I ever wrote down the details.

   I believe there is a fancy HIT in the metatheory that builds sheafification. However, I don’t think I ever wrote down the details.

3. • CommentRowNumber3.
   • CommentAuthorIngoBlechschmidt
   • CommentTimeDec 2nd 2016
   • PermaLink
   Author: IngoBlechschmidt
   Format: MarkdownItexJust 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.

   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.