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.
created predicative topos (for the entry Bishop set to link to).
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
Ieke Moerdijk, Erik Palmgren, Wellfounded trees in categories (1999) (web)
Ieke Moerdijk, Erik Palmgren, Type Theories, Toposes and Constructive Set Theory: Predicative Aspects of AST (2ooo) (web)
Definition A predicative topos is a ΠW-pretopos satisfying the axiom of multiple choice.
This is (van den Berg, def. 6.1).
So I have now been waiting 53 minutes for the page to open and now it’s there and… locked by Toby. ;-)
Not for long! (And the link powerset axiom will work properly once the Lab comes back.)
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…
Have added a bit more to the entry. Did we have an entry for $\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…
Pi-W-pretopos redirects to pretopos, where it’s just one in a line of definitions.
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).
Note that the axiom of multiple choice is also called internal WISC.
Why doesn’t the nLab call it such?
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.
But “internal”?
So I know that the “weak axiom of multiple choice” is WISC, and that’s what the $n$Lab has. But where does “internal WISC = AMC” come from? Am I mixed up?
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…
Okay. Is this explained anywhere on the $n$Lab? If not, could you add the comment?
Probably not. Will add it to the appropriate places.
Okay, thanks!
I should have been clearer, but this is what I meant to suggest in #10 with “Why doesn’t the $n$Lab 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! :-)
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 $\Pi W$-pretopos satisfying WISC. (Revert if you think this is a mistake, but I found the formulations which were there before confusing.)
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?
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.)
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.
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?
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.
I’ve added my non-example together with a reference.
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.
@Todd, sorry, yes, at predicative topos.
EDIT: I’ve now updated the existing references at WISC.
1 to 25 of 25