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

nLab > Latest Changes: predicative topos

Bottom of Page

1 to 25 of 25

  1.  
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeSep 12th 2012
    • (edited Sep 12th 2012)

    created predicative topos (for the entry Bishop set to link to).

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeSep 12th 2012
    • (edited Sep 12th 2012)

    While the lab is not responding, I’ll record my further edits here, such as not to forget about them

    The goal of a notion of predicative topos was stated in

    Definition A predicative topos is a ΠW-pretopos satisfying the axiom of multiple choice.

    This is (van den Berg, def. 6.1).

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeSep 12th 2012

    So I have now been waiting 53 minutes for the page to open and now it’s there and… locked by Toby. ;-)

    • CommentRowNumber4.
    • CommentAuthorTobyBartels
    • CommentTimeSep 12th 2012
    • (edited Sep 12th 2012)

    Not for long! (And the link powerset axiom will work properly once the Lab comes back.)

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeSep 12th 2012

    Okay. By the way, now I get the message that “The page is locked. Urs Schreiber has been editing for 9 minutes”. I wish I had…

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeSep 12th 2012

    Have added a bit more to the entry. Did we have an entry for ΠW\Pi W-toposes? I seem to recall we added some stuff about them at some point. But I am not sure if I am finding it now…

    • CommentRowNumber7.
    • CommentAuthorTobyBartels
    • CommentTimeSep 12th 2012

    Pi-W-pretopos redirects to pretopos, where it’s just one in a line of definitions.

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeSep 12th 2012

    Yes, I thought we had some more discussion of the point of it all. Probably I am thinking of the discussion at W-type.

    But I undid the redirects, now we have

    as stand-along entries (small as they may be).

    • CommentRowNumber9.
    • CommentAuthorDavidRoberts
    • CommentTimeSep 12th 2012

    Note that the axiom of multiple choice is also called internal WISC.

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeSep 12th 2012

    Why doesn’t the nLab call it such?

    • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeSep 12th 2012

    Historical reasons. Until the recent spate of papers involving Benno, AMC referred to something slightly different from internal WISC. I think they now call that version “strong AMC” and use AMC to mean internal WISC.

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeSep 13th 2012

    But “internal”?

    So I know that the “weak axiom of multiple choice” is WISC, and that’s what the nnLab has. But where does “internal WISC = AMC” come from? Am I mixed up?

    • CommentRowNumber13.
    • CommentAuthorDavidRoberts
    • CommentTimeSep 13th 2012
    • (edited Sep 13th 2012)

    External WISC is a statement about a pretopology, but internal WISC is the translation of that statement into the internal language of a pretopos. The new version of AMC is essentially just a reformulation of internal WISC into different language.

    Edit: we may not be talking about the same AMC…

    • CommentRowNumber14.
    • CommentAuthorUrs
    • CommentTimeSep 13th 2012

    Okay. Is this explained anywhere on the nnLab? If not, could you add the comment?

    • CommentRowNumber15.
    • CommentAuthorDavidRoberts
    • CommentTimeSep 13th 2012

    Probably not. Will add it to the appropriate places.

    • CommentRowNumber16.
    • CommentAuthorUrs
    • CommentTimeSep 13th 2012

    Okay, thanks!

    I should have been clearer, but this is what I meant to suggest in #10 with “Why doesn’t the nnLab say so?”.

    Because, I felt like I was already editing a lot and then you kind of threw some little fact to me here. I thought instead of throwing it at me, you would better put it right away where it belongs in the lab! :-)

    • CommentRowNumber17.
    • CommentAuthorTodd_Trimble
    • CommentTimeOct 2nd 2016

    I’m not sure what the status is now regarding the terminology, but I tried to clarify further at predicative topos and at axiom of multiple choice. I thought it clearer to say that a predicative topos (in the sense of van den Berg) is a ΠW\Pi W-pretopos satisfying WISC. (Revert if you think this is a mistake, but I found the formulations which were there before confusing.)

    • CommentRowNumber18.
    • CommentAuthorMike Shulman
    • CommentTimeOct 2nd 2016

    I think that’s right, and indeed better. It’s still a bit confusing, though, because axiom of multiple choice mentions two versions of that axiom already. Are they both the “strong” version? Are they different?

    • CommentRowNumber19.
    • CommentAuthorTodd_Trimble
    • CommentTimeOct 2nd 2016

    Oh, indeed. I didn’t try to get that sorted out, but would it be better to say “The axiom of multiple choice may mean one of several things, depending on the author…” and then follow that up with at least those two statements, and maybe a third according to van den Berg’s usage? (And at some point compare and contrast them.)

    • CommentRowNumber20.
    • CommentAuthorTodd_Trimble
    • CommentTimeOct 3rd 2016
    • (edited Oct 3rd 2016)

    Okay, I tried out a rewording of axiom of multiple choice along the lines of #18, without trying to think hard about it. It’s a little awkward still.

    • CommentRowNumber21.
    • CommentAuthorMike Shulman
    • CommentTimeOct 3rd 2016

    Yeah. I don’t really have the time to think about this right now, sadly. IIRC Benno has a formulation of WISC that refers to collection families too, perhaps making it look more like the others. Also, do we know that WISC is weaker than the others, i.e. do we have a model satisfying it but not the others?

    • CommentRowNumber22.
    • CommentAuthorDavidRoberts
    • CommentTimeOct 3rd 2016

    According to Benno, his weak AMC is equivalent to WISC. But I’m not sure in what background assumptions. As far as strong vs weak AMC goes I think he might have some means of separating them.

    • CommentRowNumber23.
    • CommentAuthorDavidRoberts
    • CommentTimeOct 3rd 2016

    I’ve added my non-example together with a reference.

    • CommentRowNumber24.
    • CommentAuthorTodd_Trimble
    • CommentTimeOct 3rd 2016

    Thanks; are you referring to what you added to predicative topos? I didn’t see anything substantive when I hit “See changes” at axiom of multiple choice.

    • CommentRowNumber25.
    • CommentAuthorDavidRoberts
    • CommentTimeOct 3rd 2016
    • (edited Oct 3rd 2016)

    @Todd, sorry, yes, at predicative topos.

    EDIT: I’ve now updated the existing references at WISC.

1 to 25 of 25

  1.