Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorUlrik
    • CommentTimeNov 21st 2016

    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?

    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeNov 21st 2016

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

  1. 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.